From 7dd6a0dcfe599778c086795cc8e15a80c6da59f5 Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Tue, 18 Feb 2025 15:46:08 +0100 Subject: [PATCH 01/14] Pallas: Add support for trap-intrinsic, fail on unknown intrinisc --- .../Instruction/IntrinsicsTransform.h | 23 ++++++++++ .../Instruction/IntrinsicsTransform.cpp | 44 +++++++++++++++++++ .../Instruction/OtherOpTransform.cpp | 3 +- 3 files changed, 69 insertions(+), 1 deletion(-) create mode 100644 src/llvm/include/Transform/Instruction/IntrinsicsTransform.h create mode 100644 src/llvm/lib/Transform/Instruction/IntrinsicsTransform.cpp diff --git a/src/llvm/include/Transform/Instruction/IntrinsicsTransform.h b/src/llvm/include/Transform/Instruction/IntrinsicsTransform.h new file mode 100644 index 000000000..039123471 --- /dev/null +++ b/src/llvm/include/Transform/Instruction/IntrinsicsTransform.h @@ -0,0 +1,23 @@ +#ifndef PALLAS_INTRINSICSTRANSFORM_H +#define PALLAS_INTRINSICSTRANSFORM_H +#include "Passes/Function/FunctionBodyTransformer.h" + +#include + +namespace llvm2col { +namespace col = vct::col::ast; + +void transformIntrinsic(llvm::CallInst &callInstruction, + col::LlvmBasicBlock &colBlock, + pallas::FunctionCursor &funcCursor); + +/** + * Transform call to the @llvm.trap()-intrinsic + */ +void transformTrap(llvm::CallInst &callInstruction, + col::LlvmBasicBlock &colBlock, + pallas::FunctionCursor &funcCursor); + +} // namespace llvm2col + +#endif // PALLAS_INTRINSICSTRANSFORM_H diff --git a/src/llvm/lib/Transform/Instruction/IntrinsicsTransform.cpp b/src/llvm/lib/Transform/Instruction/IntrinsicsTransform.cpp new file mode 100644 index 000000000..f3b228f6e --- /dev/null +++ b/src/llvm/lib/Transform/Instruction/IntrinsicsTransform.cpp @@ -0,0 +1,44 @@ +#include "Origin/OriginProvider.h" +#include "Transform/Instruction/IntrinsicsTransform.h" +#include "Transform/BlockTransform.h" +#include "Util/BlockUtils.h" + +#include +#include + +const std::string SOURCE_LOC = "Transform::Instruction::Intrinsics"; + +void llvm2col::transformIntrinsic(llvm::CallInst &callInstruction, + col::LlvmBasicBlock &colBlock, + pallas::FunctionCursor &funcCursor) { + llvm::Function *intrFunc = callInstruction.getCalledFunction(); + switch (intrFunc->getIntrinsicID()) { + case llvm::Intrinsic::trap: + transformTrap(callInstruction, colBlock, funcCursor); + break; + case llvm::Intrinsic::dbg_value: + case llvm::Intrinsic::dbg_declare: + case llvm::Intrinsic::dbg_assign: + // Ignore debug-intrinsics + break; + default: + reportUnsupportedOperatorError(SOURCE_LOC, callInstruction); + } + + // TODO: Deal with more intrinsic functions +} + +void llvm2col::transformTrap(llvm::CallInst &callInstruction, + col::LlvmBasicBlock &colBlock, + pallas::FunctionCursor &funcCursor) { + // Transform @llvm.trap() --> assert false + col::Block &body = pallas::bodyAsBlock(colBlock); + col::VctAssert *a = body.add_statements()->mutable_vct_assert(); + a->set_allocated_blame(new col::Blame()); + a->set_allocated_origin( + llvm2col::generateSingleStatementOrigin(callInstruction)); + col::BooleanValue *falseConst = a->mutable_res()->mutable_boolean_value(); + falseConst->set_value(false); + falseConst->set_allocated_origin( + llvm2col::generateSingleStatementOrigin(callInstruction)); +} diff --git a/src/llvm/lib/Transform/Instruction/OtherOpTransform.cpp b/src/llvm/lib/Transform/Instruction/OtherOpTransform.cpp index ebb059be7..b3467f0a4 100644 --- a/src/llvm/lib/Transform/Instruction/OtherOpTransform.cpp +++ b/src/llvm/lib/Transform/Instruction/OtherOpTransform.cpp @@ -10,6 +10,7 @@ #include "Passes/Function/ExprWrapperMapper.h" #include "Transform/BlockTransform.h" +#include "Transform/Instruction/IntrinsicsTransform.h" #include "Transform/Transform.h" #include "Util/BlockUtils.h" #include "Util/Constants.h" @@ -255,7 +256,7 @@ void llvm2col::transformCallExpr(llvm::CallInst &callInstruction, return; if (callInstruction.getCalledFunction()->isIntrinsic()) { - // TODO: Deal with intrinsic functions + transformIntrinsic(callInstruction, colBlock, funcCursor); return; } From 50022e0672231092089e73831552bfa90d56430c Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Tue, 18 Feb 2025 16:11:03 +0100 Subject: [PATCH 02/14] Pallas: Added support for llvm.expect intrinsic --- .../Instruction/IntrinsicsTransform.h | 7 +++++++ .../Instruction/IntrinsicsTransform.cpp | 18 +++++++++++++++++- 2 files changed, 24 insertions(+), 1 deletion(-) diff --git a/src/llvm/include/Transform/Instruction/IntrinsicsTransform.h b/src/llvm/include/Transform/Instruction/IntrinsicsTransform.h index 039123471..85f955f9a 100644 --- a/src/llvm/include/Transform/Instruction/IntrinsicsTransform.h +++ b/src/llvm/include/Transform/Instruction/IntrinsicsTransform.h @@ -18,6 +18,13 @@ void transformTrap(llvm::CallInst &callInstruction, col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); +/** + * Transform call to the @llvm.expect.XXX-intrinsic + */ +void transformExpect(llvm::CallInst &callInstruction, + col::LlvmBasicBlock &colBlock, + pallas::FunctionCursor &funcCursor); + } // namespace llvm2col #endif // PALLAS_INTRINSICSTRANSFORM_H diff --git a/src/llvm/lib/Transform/Instruction/IntrinsicsTransform.cpp b/src/llvm/lib/Transform/Instruction/IntrinsicsTransform.cpp index f3b228f6e..f4eaea7f7 100644 --- a/src/llvm/lib/Transform/Instruction/IntrinsicsTransform.cpp +++ b/src/llvm/lib/Transform/Instruction/IntrinsicsTransform.cpp @@ -1,6 +1,7 @@ -#include "Origin/OriginProvider.h" #include "Transform/Instruction/IntrinsicsTransform.h" +#include "Origin/OriginProvider.h" #include "Transform/BlockTransform.h" +#include "Transform/Transform.h" #include "Util/BlockUtils.h" #include @@ -16,6 +17,9 @@ void llvm2col::transformIntrinsic(llvm::CallInst &callInstruction, case llvm::Intrinsic::trap: transformTrap(callInstruction, colBlock, funcCursor); break; + case llvm::Intrinsic::expect: + transformExpect(callInstruction, colBlock, funcCursor); + break; case llvm::Intrinsic::dbg_value: case llvm::Intrinsic::dbg_declare: case llvm::Intrinsic::dbg_assign: @@ -42,3 +46,15 @@ void llvm2col::transformTrap(llvm::CallInst &callInstruction, falseConst->set_allocated_origin( llvm2col::generateSingleStatementOrigin(callInstruction)); } + +void llvm2col::transformExpect(llvm::CallInst &callInstruction, + col::LlvmBasicBlock &colBlock, + pallas::FunctionCursor &funcCursor) { + // Transform %x2 = call XXX @llvm.expect.XXX(%x1, YYY) --> x2 = x1; + col::Assign &assignment = funcCursor.createAssignmentAndDeclaration( + callInstruction, colBlock); + // auto *assignExpr = assignment.mutable_value(); + llvm2col::transformAndSetExpr(funcCursor, callInstruction, + *callInstruction.getArgOperand(0), + *assignment.mutable_value()); +} From c4dc6afe56c3d0d7b112ee6f55d0d63d23878f6f Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Thu, 20 Feb 2025 13:01:42 +0100 Subject: [PATCH 03/14] Skip the entry-global from Swift for now. --- src/llvm/include/Util/Constants.h | 4 ++++ src/llvm/lib/Passes/Module/GlobalVariableDeclarer.cpp | 6 ++++++ 2 files changed, 10 insertions(+) diff --git a/src/llvm/include/Util/Constants.h b/src/llvm/include/Util/Constants.h index 409812e73..00cf0cce1 100644 --- a/src/llvm/include/Util/Constants.h +++ b/src/llvm/include/Util/Constants.h @@ -37,6 +37,10 @@ const std::string VC_PREFIX = "VC."; const std::string METADATA_PURE_KEYWORD = VC_PREFIX + "pure"; const std::string METADATA_CONTRACT_KEYWORD = VC_PREFIX + "contract"; const std::string METADATA_GLOBAL_KEYWORD = VC_PREFIX + "global"; + +// Other constants +const std::string SWIFT_ENTRY_SECTION = "swift5_entry"; + } // namespace pallas::constants #endif // PALLAS_CONSTANTS_H diff --git a/src/llvm/lib/Passes/Module/GlobalVariableDeclarer.cpp b/src/llvm/lib/Passes/Module/GlobalVariableDeclarer.cpp index e79f35190..f09453445 100644 --- a/src/llvm/lib/Passes/Module/GlobalVariableDeclarer.cpp +++ b/src/llvm/lib/Passes/Module/GlobalVariableDeclarer.cpp @@ -1,6 +1,7 @@ #include "Passes/Module/GlobalVariableDeclarer.h" #include "Passes/Module/RootContainer.h" #include "Transform/Transform.h" +#include "Util/Constants.h" namespace pallas { const std::string SOURCE_LOC = "Passes::Module::GlobalVariableDeclarer"; @@ -12,6 +13,11 @@ PreservedAnalyses GlobalVariableDeclarerPass::run(Module &M, auto pProgram = MAM.getResult(M).program; for (auto &global : M.globals()) { + // Skip the entry-point global from swift, as it contains currently + // unsupported poitner-casting and is not needed for verification. + if (global.getSection().str() == constants::SWIFT_ENTRY_SECTION) + continue; + col::GlobalDeclaration *globDecl = pProgram->add_declarations(); col::LlvmGlobalVariable *colGlobal = globDecl->mutable_llvm_global_variable(); From 083641d3dbb3c56c0259b2e8c14e81910772efa0 Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Fri, 21 Feb 2025 12:37:38 +0100 Subject: [PATCH 04/14] Pallas: Added support of arithmetic intrinsics with overflow --- src/col/vct/col/ast/Node.scala | 27 ++++ .../lang/llvm/LLVMAddWithOverflowImpl.scala | 13 ++ .../llvm/LLVMArithOpWithOverflowImpl.scala | 23 ++++ .../lang/llvm/LLVMMultWithOverflowImpl.scala | 12 ++ .../lang/llvm/LLVMSubWithOverflowImpl.scala | 12 ++ .../Instruction/IntrinsicsTransform.h | 24 ++++ .../Passes/Module/GlobalVariableDeclarer.cpp | 4 +- .../Instruction/IntrinsicsTransform.cpp | 116 +++++++++++++++++- .../vct/rewrite/lang/LangLLVMToCol.scala | 58 +++++++++ .../vct/rewrite/lang/LangSpecificToCol.scala | 3 + 10 files changed, 285 insertions(+), 7 deletions(-) create mode 100644 src/col/vct/col/ast/lang/llvm/LLVMAddWithOverflowImpl.scala create mode 100644 src/col/vct/col/ast/lang/llvm/LLVMArithOpWithOverflowImpl.scala create mode 100644 src/col/vct/col/ast/lang/llvm/LLVMMultWithOverflowImpl.scala create mode 100644 src/col/vct/col/ast/lang/llvm/LLVMSubWithOverflowImpl.scala diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index 12ab163b5..6dc11d927 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -3795,6 +3795,33 @@ final case class LLVMFloatExtend[G]( )(implicit val o: Origin) extends LLVMExpr[G] with LLVMFloatExtendImpl[G] +sealed trait LLVMArithOpWithOverflow[G] + extends LLVMStatement[G] with LLVMArithOpWithOverflowImpl[G] + +final case class LLVMAddWithOverflow[G]( + target: Expr[G], + left: Expr[G], + right: Expr[G], + signed: Boolean, +)(val blame: Blame[AssignFailed])(implicit val o: Origin) + extends LLVMArithOpWithOverflow[G] with LLVMAddWithOverflowImpl[G] + +final case class LLVMSubWithOverflow[G]( + target: Expr[G], + left: Expr[G], + right: Expr[G], + signed: Boolean, +)(val blame: Blame[AssignFailed])(implicit val o: Origin) + extends LLVMArithOpWithOverflow[G] with LLVMSubWithOverflowImpl[G] + +final case class LLVMMultWithOverflow[G]( + target: Expr[G], + left: Expr[G], + right: Expr[G], + signed: Boolean, +)(val blame: Blame[AssignFailed])(implicit val o: Origin) + extends LLVMArithOpWithOverflow[G] with LLVMMultWithOverflowImpl[G] + final class LLVMGlobalSpecification[G](val value: String)( implicit val o: Origin ) extends GlobalDeclaration[G] with LLVMGlobalSpecificationImpl[G] { diff --git a/src/col/vct/col/ast/lang/llvm/LLVMAddWithOverflowImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMAddWithOverflowImpl.scala new file mode 100644 index 000000000..5a15460b6 --- /dev/null +++ b/src/col/vct/col/ast/lang/llvm/LLVMAddWithOverflowImpl.scala @@ -0,0 +1,13 @@ +package vct.col.ast.lang.llvm + +import vct.col.ast.LLVMAddWithOverflow +import vct.col.ast.ops.LLVMAddWithOverflowOps +import vct.col.print._ + +trait LLVMAddWithOverflowImpl[G] extends LLVMAddWithOverflowOps[G] { + this: LLVMAddWithOverflow[G] => + override def instRepr: Doc = + if (signed) { Text("sadd.with.overflow") } + else { Text("uadd.with.overflow") } + +} diff --git a/src/col/vct/col/ast/lang/llvm/LLVMArithOpWithOverflowImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMArithOpWithOverflowImpl.scala new file mode 100644 index 000000000..17efc264d --- /dev/null +++ b/src/col/vct/col/ast/lang/llvm/LLVMArithOpWithOverflowImpl.scala @@ -0,0 +1,23 @@ +package vct.col.ast.lang.llvm + +import vct.col.ast.{Expr, LLVMArithOpWithOverflow} +import vct.col.origin.{AssignFailed, Blame} +import vct.col.print._ + +trait LLVMArithOpWithOverflowImpl[G] { + this: LLVMArithOpWithOverflow[G] => + def target: Expr[G] + def left: Expr[G] + def right: Expr[G] + def signed: Boolean + def blame: Blame[AssignFailed] + + def instRepr: Doc + + override def layout(implicit ctx: Ctx): Doc = { + Group( + target.show <+> Text("=") <+> instRepr <+> Text("(") <+> left.show <+> + Text(", ") <+> right.show <+> Text(")") + ) + } +} diff --git a/src/col/vct/col/ast/lang/llvm/LLVMMultWithOverflowImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMMultWithOverflowImpl.scala new file mode 100644 index 000000000..a55675af3 --- /dev/null +++ b/src/col/vct/col/ast/lang/llvm/LLVMMultWithOverflowImpl.scala @@ -0,0 +1,12 @@ +package vct.col.ast.lang.llvm + +import vct.col.ast.ops.LLVMMultWithOverflowOps +import vct.col.ast.{LLVMMultWithOverflow, Type} +import vct.col.print._ + +trait LLVMMultWithOverflowImpl[G] extends LLVMMultWithOverflowOps[G] { + this: LLVMMultWithOverflow[G] => + override def instRepr: Doc = + if (signed) { Text("smul.with.overflow") } + else { Text("umul.with.overflow") } +} diff --git a/src/col/vct/col/ast/lang/llvm/LLVMSubWithOverflowImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMSubWithOverflowImpl.scala new file mode 100644 index 000000000..221e3ff11 --- /dev/null +++ b/src/col/vct/col/ast/lang/llvm/LLVMSubWithOverflowImpl.scala @@ -0,0 +1,12 @@ +package vct.col.ast.lang.llvm + +import vct.col.ast.LLVMSubWithOverflow +import vct.col.ast.ops.LLVMSubWithOverflowOps +import vct.col.print._ + +trait LLVMSubWithOverflowImpl[G] extends LLVMSubWithOverflowOps[G] { + this: LLVMSubWithOverflow[G] => + override def instRepr: Doc = + if (signed) { Text("ssub.with.overflow") } + else { Text("usub.with.overflow") } +} diff --git a/src/llvm/include/Transform/Instruction/IntrinsicsTransform.h b/src/llvm/include/Transform/Instruction/IntrinsicsTransform.h index 85f955f9a..0f20efb98 100644 --- a/src/llvm/include/Transform/Instruction/IntrinsicsTransform.h +++ b/src/llvm/include/Transform/Instruction/IntrinsicsTransform.h @@ -25,6 +25,30 @@ void transformExpect(llvm::CallInst &callInstruction, col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); +/** + * Transform call to the @llvm.sadd.with.overflow or + * @llvm.uadd.with.overflow-intrinsic + */ +void transformAddWithOverflow(llvm::CallInst &callInstruction, + col::LlvmBasicBlock &colBlock, + pallas::FunctionCursor &funcCursor, bool sign); + +/** + * Transform call to the @llvm.ssub.with.overflow or + * @llvm.usub.with.overflow-intrinsic + */ +void transformSubWithOverflow(llvm::CallInst &callInstruction, + col::LlvmBasicBlock &colBlock, + pallas::FunctionCursor &funcCursor, bool sign); + +/** + * Transform call to the @llvm.smult.with.overflow or + * @llvm.umult.with.overflow-intrinsic + */ +void transformMultWithOverflow(llvm::CallInst &callInstruction, + col::LlvmBasicBlock &colBlock, + pallas::FunctionCursor &funcCursor, bool sign); + } // namespace llvm2col #endif // PALLAS_INTRINSICSTRANSFORM_H diff --git a/src/llvm/lib/Passes/Module/GlobalVariableDeclarer.cpp b/src/llvm/lib/Passes/Module/GlobalVariableDeclarer.cpp index f09453445..bbfd56cea 100644 --- a/src/llvm/lib/Passes/Module/GlobalVariableDeclarer.cpp +++ b/src/llvm/lib/Passes/Module/GlobalVariableDeclarer.cpp @@ -13,11 +13,11 @@ PreservedAnalyses GlobalVariableDeclarerPass::run(Module &M, auto pProgram = MAM.getResult(M).program; for (auto &global : M.globals()) { - // Skip the entry-point global from swift, as it contains currently + // Skip the entry-point global from swift, as it contains currently // unsupported poitner-casting and is not needed for verification. if (global.getSection().str() == constants::SWIFT_ENTRY_SECTION) continue; - + col::GlobalDeclaration *globDecl = pProgram->add_declarations(); col::LlvmGlobalVariable *colGlobal = globDecl->mutable_llvm_global_variable(); diff --git a/src/llvm/lib/Transform/Instruction/IntrinsicsTransform.cpp b/src/llvm/lib/Transform/Instruction/IntrinsicsTransform.cpp index f4eaea7f7..c11eecccf 100644 --- a/src/llvm/lib/Transform/Instruction/IntrinsicsTransform.cpp +++ b/src/llvm/lib/Transform/Instruction/IntrinsicsTransform.cpp @@ -6,6 +6,7 @@ #include #include +#include const std::string SOURCE_LOC = "Transform::Instruction::Intrinsics"; @@ -20,6 +21,24 @@ void llvm2col::transformIntrinsic(llvm::CallInst &callInstruction, case llvm::Intrinsic::expect: transformExpect(callInstruction, colBlock, funcCursor); break; + case llvm::Intrinsic::sadd_with_overflow: + transformAddWithOverflow(callInstruction, colBlock, funcCursor, true); + break; + case llvm::Intrinsic::uadd_with_overflow: + transformAddWithOverflow(callInstruction, colBlock, funcCursor, false); + break; + case llvm::Intrinsic::ssub_with_overflow: + transformSubWithOverflow(callInstruction, colBlock, funcCursor, true); + break; + case llvm::Intrinsic::usub_with_overflow: + transformSubWithOverflow(callInstruction, colBlock, funcCursor, false); + break; + case llvm::Intrinsic::smul_with_overflow: + transformMultWithOverflow(callInstruction, colBlock, funcCursor, true); + break; + case llvm::Intrinsic::umul_with_overflow: + transformMultWithOverflow(callInstruction, colBlock, funcCursor, false); + break; case llvm::Intrinsic::dbg_value: case llvm::Intrinsic::dbg_declare: case llvm::Intrinsic::dbg_assign: @@ -51,10 +70,97 @@ void llvm2col::transformExpect(llvm::CallInst &callInstruction, col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { // Transform %x2 = call XXX @llvm.expect.XXX(%x1, YYY) --> x2 = x1; - col::Assign &assignment = funcCursor.createAssignmentAndDeclaration( - callInstruction, colBlock); - // auto *assignExpr = assignment.mutable_value(); + col::Assign &assignment = + funcCursor.createAssignmentAndDeclaration(callInstruction, colBlock); + // auto *assignExpr = assignment.mutable_value(); + llvm2col::transformAndSetExpr(funcCursor, callInstruction, + *callInstruction.getArgOperand(0), + *assignment.mutable_value()); +} + +void llvm2col::transformAddWithOverflow(llvm::CallInst &callInstruction, + col::LlvmBasicBlock &colBlock, + pallas::FunctionCursor &funcCursor, + bool sign) { + llvm::Function *intrFunc = callInstruction.getCalledFunction(); + col::Block &body = pallas::bodyAsBlock(colBlock); + col::Variable &targetVar = funcCursor.declareVariable(callInstruction); + col::LlvmAddWithOverflow *add = + body.add_statements()->mutable_llvm_add_with_overflow(); + add->set_allocated_origin( + llvm2col::generateSingleStatementOrigin(callInstruction)); + add->set_allocated_blame(new col::Blame()); + // signed + add->set_signed_(sign); + // target + col::Local *targetLocal = add->mutable_target()->mutable_local(); + targetLocal->set_allocated_origin( + llvm2col::generateAssignTargetOrigin(callInstruction)); + targetLocal->mutable_ref()->set_id(targetVar.id()); + // left + llvm2col::transformAndSetExpr(funcCursor, callInstruction, + *callInstruction.getArgOperand(0), + *add->mutable_left()); + // right + llvm2col::transformAndSetExpr(funcCursor, callInstruction, + *callInstruction.getArgOperand(1), + *add->mutable_right()); +} + +void llvm2col::transformSubWithOverflow(llvm::CallInst &callInstruction, + col::LlvmBasicBlock &colBlock, + pallas::FunctionCursor &funcCursor, + bool sign) { + llvm::Function *intrFunc = callInstruction.getCalledFunction(); + col::Block &body = pallas::bodyAsBlock(colBlock); + col::Variable &targetVar = funcCursor.declareVariable(callInstruction); + col::LlvmSubWithOverflow *sub = + body.add_statements()->mutable_llvm_sub_with_overflow(); + sub->set_allocated_origin( + llvm2col::generateSingleStatementOrigin(callInstruction)); + sub->set_allocated_blame(new col::Blame()); + // signed + sub->set_signed_(sign); + // target + col::Local *targetLocal = sub->mutable_target()->mutable_local(); + targetLocal->set_allocated_origin( + llvm2col::generateAssignTargetOrigin(callInstruction)); + targetLocal->mutable_ref()->set_id(targetVar.id()); + // left + llvm2col::transformAndSetExpr(funcCursor, callInstruction, + *callInstruction.getArgOperand(0), + *sub->mutable_left()); + // right + llvm2col::transformAndSetExpr(funcCursor, callInstruction, + *callInstruction.getArgOperand(1), + *sub->mutable_right()); +} + +void llvm2col::transformMultWithOverflow(llvm::CallInst &callInstruction, + col::LlvmBasicBlock &colBlock, + pallas::FunctionCursor &funcCursor, + bool sign) { + llvm::Function *intrFunc = callInstruction.getCalledFunction(); + col::Block &body = pallas::bodyAsBlock(colBlock); + col::Variable &targetVar = funcCursor.declareVariable(callInstruction); + col::LlvmMultWithOverflow *mult = + body.add_statements()->mutable_llvm_mult_with_overflow(); + mult->set_allocated_origin( + llvm2col::generateSingleStatementOrigin(callInstruction)); + mult->set_allocated_blame(new col::Blame()); + // signed + mult->set_signed_(sign); + // target + col::Local *targetLocal = mult->mutable_target()->mutable_local(); + targetLocal->set_allocated_origin( + llvm2col::generateAssignTargetOrigin(callInstruction)); + targetLocal->mutable_ref()->set_id(targetVar.id()); + // left + llvm2col::transformAndSetExpr(funcCursor, callInstruction, + *callInstruction.getArgOperand(0), + *mult->mutable_left()); + // right llvm2col::transformAndSetExpr(funcCursor, callInstruction, - *callInstruction.getArgOperand(0), - *assignment.mutable_value()); + *callInstruction.getArgOperand(1), + *mult->mutable_right()); } diff --git a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala index b5e193da7..7590b9fda 100644 --- a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala @@ -947,6 +947,64 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) CastFloat(rw.dispatch(fpext.value), rw.dispatch(fpext.t)) } + def rewriteArithOpWithOverflow( + instr: LLVMArithOpWithOverflow[Pre], + op: (Expr[Post], Expr[Post]) => Expr[Post], + ) = { + implicit val o: Origin = instr.o + // TODO: Do not ignore the signedness + val targetStructT = + instr.target.t match { + case s: LLVMTStruct[Pre] => s + case _ => ??? // Should never happen + } + // Assign new object to target + val newCls = structMap.get(targetStructT).get + val assignNew = + Assign(rw.dispatch(instr.target), new NewObject[Post](newCls.ref))( + instr.blame + ) + // Set result-field + val resField = structFieldMap((targetStructT, 0)) + val assignRes = + Assign( + Deref[Post](rw.dispatch(instr.target), resField.ref)(PanicBlame( + "Generated object always has permissions" + )), + op(rw.dispatch(instr.left), rw.dispatch(instr.right)), + )(instr.blame) + + // Set overflow-flag + val flagField = structFieldMap((targetStructT, 1)) + val assignFlag = + Assign( + Deref[Post](rw.dispatch(instr.target), flagField.ref)(PanicBlame( + "Generated object always has permissions" + )), + ff, + )(instr.blame) + + // Build Block + Block(Seq(assignNew, assignRes, assignFlag)) + } + + def rewriteAddWithOverflow(add: LLVMAddWithOverflow[Pre]): Statement[Post] = { + implicit val o: Origin = add.o + rewriteArithOpWithOverflow(add, (l, r) => l + r) + } + + def rewriteSubWithOverflow(sub: LLVMSubWithOverflow[Pre]): Statement[Post] = { + implicit val o: Origin = sub.o + rewriteArithOpWithOverflow(sub, (l, r) => l - r) + } + + def rewriteMultWithOverflow( + mult: LLVMMultWithOverflow[Pre] + ): Statement[Post] = { + implicit val o: Origin = mult.o + rewriteArithOpWithOverflow(mult, (l, r) => l * r) + } + def rewriteUnreachable( unreachable: LLVMBranchUnreachable[Pre] ): Statement[Post] = { diff --git a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala index d2ec9e2b3..029650630 100644 --- a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala @@ -339,6 +339,9 @@ case class LangSpecificToCol[Pre <: Generation]( case unreachable: LLVMBranchUnreachable[Pre] => llvm.rewriteUnreachable(unreachable) case fracOf: LLVMFracOf[Pre] => llvm.rewriteFracOf(fracOf) + case add: LLVMAddWithOverflow[Pre] => llvm.rewriteAddWithOverflow(add) + case sub: LLVMSubWithOverflow[Pre] => llvm.rewriteSubWithOverflow(sub) + case mult: LLVMMultWithOverflow[Pre] => llvm.rewriteMultWithOverflow(mult) case other => other.rewriteDefault() } From 6e2fe6ef451a18df2f84433f4cea328138881f0c Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Fri, 21 Feb 2025 16:15:37 +0100 Subject: [PATCH 05/14] Pallas: Draft for extractvalue-support --- src/col/vct/col/ast/Node.scala | 8 +++ .../ast/lang/llvm/LLVMExtractValueImpl.scala | 14 +++++ .../Transform/Instruction/OtherOpTransform.h | 4 ++ .../Instruction/OtherOpTransform.cpp | 31 +++++++++++ .../vct/rewrite/lang/LangLLVMToCol.scala | 55 +++++++++++++++---- .../vct/rewrite/lang/LangSpecificToCol.scala | 1 + 6 files changed, 103 insertions(+), 10 deletions(-) create mode 100644 src/col/vct/col/ast/lang/llvm/LLVMExtractValueImpl.scala diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index 6dc11d927..cfa952d56 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -3767,6 +3767,14 @@ final case class LLVMGetElementPointer[G]( )(implicit val o: Origin) extends LLVMExpr[G] with LLVMGetElementPointerImpl[G] +final case class LLVMExtractValue[G]( + aggregateType: Type[G], + resultType: Type[G], + value: Expr[G], + indices: Seq[Int], +)(implicit val o: Origin) + extends LLVMExpr[G] with LLVMExtractValueImpl[G] + final case class LLVMSignExtend[G]( inputType: Type[G], outputType: Type[G], diff --git a/src/col/vct/col/ast/lang/llvm/LLVMExtractValueImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMExtractValueImpl.scala new file mode 100644 index 000000000..a55710b54 --- /dev/null +++ b/src/col/vct/col/ast/lang/llvm/LLVMExtractValueImpl.scala @@ -0,0 +1,14 @@ +package vct.col.ast.lang.llvm + +import vct.col.ast.LLVMExtractValue +import vct.col.ast.ops.LLVMExtractValueOps +import vct.col.print._ + +trait LLVMExtractValueImpl[G] extends LLVMExtractValueOps[G] { + this: LLVMExtractValue[G] => + + override def layout(implicit ctx: Ctx): Doc = + Text("extractValue<") <+> aggregateType <> ">" <+> value.show <> "[" <+> + Doc.args(indices.map(i => Text(i.toString))) <+> "]" + override def t = resultType +} diff --git a/src/llvm/include/Transform/Instruction/OtherOpTransform.h b/src/llvm/include/Transform/Instruction/OtherOpTransform.h index a04d06bbe..42d6f5d14 100644 --- a/src/llvm/include/Transform/Instruction/OtherOpTransform.h +++ b/src/llvm/include/Transform/Instruction/OtherOpTransform.h @@ -33,6 +33,10 @@ void transformICmp(llvm::ICmpInst &icmpInstruction, void transformCmpExpr(llvm::CmpInst &cmpInstruction, auto &colCompareExpr, pallas::FunctionCursor &funcCursor); +void transformExtractValueInst(llvm::ExtractValueInst &llvmInstruction, + col::LlvmBasicBlock &colBlock, + pallas::FunctionCursor &funcCursor); + void transformCallExpr(llvm::CallInst &callInstruction, col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); diff --git a/src/llvm/lib/Transform/Instruction/OtherOpTransform.cpp b/src/llvm/lib/Transform/Instruction/OtherOpTransform.cpp index b3467f0a4..d970fdf8c 100644 --- a/src/llvm/lib/Transform/Instruction/OtherOpTransform.cpp +++ b/src/llvm/lib/Transform/Instruction/OtherOpTransform.cpp @@ -39,6 +39,11 @@ void llvm2col::transformOtherOp(llvm::Instruction &llvmInstruction, transformCallExpr(llvm::cast(llvmInstruction), colBlock, funcCursor); break; + case llvm::Instruction::ExtractValue: + transformExtractValueInst( + llvm::cast(llvmInstruction), colBlock, + funcCursor); + break; default: reportUnsupportedOperatorError(SOURCE_LOC, llvmInstruction); } @@ -204,6 +209,32 @@ void llvm2col::transformCmpExpr(llvm::CmpInst &cmpInstruction, transformBinExpr(cmpInstruction, colCompareExpr, funcCursor); } +void llvm2col::transformExtractValueInst( + llvm::ExtractValueInst &llvmInstruction, col::LlvmBasicBlock &colBlock, + pallas::FunctionCursor &funcCursor) { + col::Assign &assignment = + funcCursor.createAssignmentAndDeclaration(llvmInstruction, colBlock); + col::LlvmExtractValue *extrVal = + assignment.mutable_value()->mutable_llvm_extract_value(); + extrVal->set_allocated_origin( + llvm2col::generateSingleStatementOrigin(llvmInstruction)); + // Aggregate type + llvm2col::transformAndSetType( + *llvmInstruction.getAggregateOperand()->getType(), + *extrVal->mutable_aggregate_type()); + // Result type + llvm2col::transformAndSetType(*llvmInstruction.getType(), + *extrVal->mutable_result_type()); + // Value + llvm2col::transformAndSetExpr(funcCursor, llvmInstruction, + *llvmInstruction.getAggregateOperand(), + *extrVal->mutable_value()); + // Indices + for (auto &index : llvmInstruction.indices()) { + extrVal->add_indices(index); + } +} + bool llvm2col::checkCallSupport(llvm::CallInst &callInstruction) { if (callInstruction.isIndirectCall()) { pallas::ErrorReporter::addError( diff --git a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala index 7590b9fda..4ee064f7d 100644 --- a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala @@ -73,6 +73,14 @@ case object LangLLVMToCol { ) } + private final case class UnsupportedExtractValueType(o: Origin) + extends UserError { + override def code: String = "unsupportedExtractValueType" + + override def text: String = + o.messageInContext(s"Unsupported aggregate-type used in extractvalue") + } + private final case class UnreachableReached( unreachable: LLVMBranchUnreachable[_] ) extends Blame[AssertFailed] { @@ -80,13 +88,14 @@ case object LangLLVMToCol { unreachable.blame.blame(UnreachableReachedError(unreachable)) } - val pallasResArgPermOrigin: Origin = Origin(Seq( + private val pallasResArgPermOrigin: Origin = Origin(Seq( PreferredName(Seq("resArg context")), LabelContext("Generated context for resArg"), )) // TODO: This should be replaced with the correct blames! - object InvalidGEP extends PanicBlame("Invalid use of getelementpointer!") + private object InvalidGEP + extends PanicBlame("Invalid use of getelementpointer!") } case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) @@ -449,7 +458,7 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) } def rewriteLocalVariable(v: Variable[Pre]): Unit = { - implicit val o: Origin = v.o; + implicit val o: Origin = v.o rw.variables.succeed(v, new Variable[Post](rw.dispatch(getLocalVarType(v)))) } @@ -905,6 +914,32 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) // Deref might not be the correct thing to use here since technically the pointer is only dereferenced in the load or store instruction } + def derefStructIndexChain(value: Expr[Post], t: Type[Pre], indices: Seq[Int])( + implicit o: Origin + ): Expr[Post] = { + if (indices.isEmpty) { return value } + t match { + case struct: LLVMTStruct[Pre] => + if (!structMap.contains(struct)) { rewriteStruct(struct) } + val idx = indices.head + derefStructIndexChain( + Deref[Post](value, structFieldMap.ref((struct, idx)))(InvalidGEP), + struct.elements(idx), + indices.tail, + ) + case _ => throw UnsupportedExtractValueType(o) + } + } + + def rewriteExtractValue(extrVal: LLVMExtractValue[Pre]): Expr[Post] = { + implicit val o: Origin = extrVal.o + derefStructIndexChain( + rw.dispatch(extrVal.value), + extrVal.aggregateType, + extrVal.indices, + ) + } + def rewriteSignExtend(sext: LLVMSignExtend[Pre]): Expr[Post] = { implicit val o: Origin = sext.o // As long as we don't support integers as bitvectors this is mostly a no-op @@ -947,7 +982,7 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) CastFloat(rw.dispatch(fpext.value), rw.dispatch(fpext.t)) } - def rewriteArithOpWithOverflow( + private def rewriteArithOpWithOverflow( instr: LLVMArithOpWithOverflow[Pre], op: (Expr[Post], Expr[Post]) => Expr[Post], ) = { @@ -1259,13 +1294,13 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) implicit o: Origin ): Expr[Post] = Result[Post](llvmFunctionMap.ref(ref.decl)) - def phiTmpVarOrigin() = + private def phiTmpVarOrigin() = Origin(Seq( PreferredName(Seq("phiTmp")), LabelContext(s"Generated tmp-var for phi-assignment"), )) - def phiTmpVarAssignOrigin() = + private def phiTmpVarAssignOrigin() = Origin(Seq(LabelContext(s"Generated assignment to tmp-var for phi-node"))) private def buildPhiAssignments( @@ -1385,8 +1420,8 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) Loop restructuring should be handled by Pallas as it has much more analytical and contextual information about the program. */ - case class GotoEliminator(bodyScope: Scope[Pre]) extends LazyLogging { - val labelDeclMap: Map[LabelDecl[Pre], LLVMBasicBlock[Pre]] = + private case class GotoEliminator(bodyScope: Scope[Pre]) extends LazyLogging { + private val labelDeclMap: Map[LabelDecl[Pre], LLVMBasicBlock[Pre]] = bodyScope.body match { case block: Block[Pre] => block.statements.map { @@ -1414,7 +1449,7 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) } } - def eliminate(bb: LLVMBasicBlock[Pre]): Block[Post] = { + private def eliminate(bb: LLVMBasicBlock[Pre]): Block[Post] = { implicit val o: Origin = bb.o bb.terminator match { case goto: Goto[Pre] => @@ -1436,7 +1471,7 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) } } - def eliminate(branch: Branch[Pre]): Branch[Post] = { + private def eliminate(branch: Branch[Pre]): Branch[Post] = { implicit val o: Origin = branch.o Branch[Post](branch.branches.map(bs => ( diff --git a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala index 029650630..a87c0286f 100644 --- a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala @@ -452,6 +452,7 @@ case class LangSpecificToCol[Pre <: Generation]( llvm.rewriteFunctionPointer(pointer) case pointer: LLVMPointerValue[Pre] => llvm.rewritePointerValue(pointer) case gep: LLVMGetElementPointer[Pre] => llvm.rewriteGetElementPointer(gep) + case extrVal: LLVMExtractValue[Pre] => llvm.rewriteExtractValue(extrVal) case int: LLVMIntegerValue[Pre] => IntegerValue(int.value)(int.o) case float: LLVMFloatValue[Pre] => FloatValue(float.bigDecimalValue, dispatch(float.t))(float.o) From c3c95bcbc534406f3ac3448cdc80cc58f6e0ded2 Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Mon, 24 Feb 2025 12:40:02 +0100 Subject: [PATCH 06/14] Pallas: replace fatalError of Swift with requires false-contract --- src/llvm/include/Util/Constants.h | 2 ++ .../lib/Passes/Function/FunctionBodyTransformer.cpp | 11 +++++++++++ .../lib/Passes/Function/FunctionContractDeclarer.cpp | 12 ++++++++++++ .../lib/Transform/Instruction/OtherOpTransform.cpp | 4 ++-- 4 files changed, 27 insertions(+), 2 deletions(-) diff --git a/src/llvm/include/Util/Constants.h b/src/llvm/include/Util/Constants.h index 00cf0cce1..bfcfccb15 100644 --- a/src/llvm/include/Util/Constants.h +++ b/src/llvm/include/Util/Constants.h @@ -40,6 +40,8 @@ const std::string METADATA_GLOBAL_KEYWORD = VC_PREFIX + "global"; // Other constants const std::string SWIFT_ENTRY_SECTION = "swift5_entry"; +const std::string SWIFT_FATAL_ERROR = + "$ss10fatalError_4file4lines5NeverOSSyXK_s12StaticStringVSutFfA_SSycfu_"; } // namespace pallas::constants diff --git a/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp b/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp index d58489e42..6284d9fb8 100644 --- a/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp +++ b/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp @@ -6,6 +6,7 @@ #include "Transform/BlockTransform.h" #include "Transform/Transform.h" #include "Util/BlockUtils.h" +#include "Util/Constants.h" #include "Util/Exceptions.h" #include @@ -203,6 +204,16 @@ FunctionBodyTransformerPass::run(Function &F, FunctionAnalysisManager &FAM) { funcCursor.addVariableMapEntry( A, FAM.getResult(F).getFuncArgMapEntry(A)); } + + // Skip the body of the fatalError-function from Swift + // (As it uses currently unsupported instructions). We generate an + // requires false; - contract instead. + if (F.getName().str() == constants::SWIFT_FATAL_ERROR) { + ErrorReporter::addWarning( + SOURCE_LOC, "Skipping body of swift fatalError", F); + return PreservedAnalyses::all(); + } + // start recursive block code gen with basic block llvm::BasicBlock &entryBlock = F.getEntryBlock(); llvm2col::transformLLVMBlock(entryBlock, funcCursor); diff --git a/src/llvm/lib/Passes/Function/FunctionContractDeclarer.cpp b/src/llvm/lib/Passes/Function/FunctionContractDeclarer.cpp index 533659709..bd0b792bb 100644 --- a/src/llvm/lib/Passes/Function/FunctionContractDeclarer.cpp +++ b/src/llvm/lib/Passes/Function/FunctionContractDeclarer.cpp @@ -49,6 +49,18 @@ FunctionContractDeclarerPass::run(Function &F, FunctionAnalysisManager &FAM) { .mutable_vcllvm_function_contract(); colContract->set_allocated_blame(new col::Blame()); colContract->set_name(F.getName()); + + // Add a "requires false"-contract to Swift's fatalError-function + // (Since we currently do not support all instructions that it uses). + if (F.getName().str() == constants::SWIFT_FATAL_ERROR) { + ErrorReporter::addWarning( + SOURCE_LOC, "Generating contract forswift fatalError", F); + colContract->set_value("requires false;"); + colContract->set_allocated_origin( + llvm2col::generateFunctionContractOrigin(F, "requires false;")); + return PreservedAnalyses::all(); + } + // check if contract keyword is present if (!F.hasMetadata(pallas::constants::METADATA_CONTRACT_KEYWORD)) { // set contract to a tautology diff --git a/src/llvm/lib/Transform/Instruction/OtherOpTransform.cpp b/src/llvm/lib/Transform/Instruction/OtherOpTransform.cpp index d970fdf8c..514848e69 100644 --- a/src/llvm/lib/Transform/Instruction/OtherOpTransform.cpp +++ b/src/llvm/lib/Transform/Instruction/OtherOpTransform.cpp @@ -227,8 +227,8 @@ void llvm2col::transformExtractValueInst( *extrVal->mutable_result_type()); // Value llvm2col::transformAndSetExpr(funcCursor, llvmInstruction, - *llvmInstruction.getAggregateOperand(), - *extrVal->mutable_value()); + *llvmInstruction.getAggregateOperand(), + *extrVal->mutable_value()); // Indices for (auto &index : llvmInstruction.indices()) { extrVal->add_indices(index); From 7e939fb1254372dc264a16945341ce459e99782e Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Mon, 24 Feb 2025 12:59:45 +0100 Subject: [PATCH 07/14] Pallas: Skip memory-lifetime intrinsics --- src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp | 4 ++-- src/llvm/lib/Passes/Function/FunctionContractDeclarer.cpp | 6 +++--- src/llvm/lib/Transform/Instruction/IntrinsicsTransform.cpp | 4 ++++ 3 files changed, 9 insertions(+), 5 deletions(-) diff --git a/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp b/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp index 6284d9fb8..c72bf9f33 100644 --- a/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp +++ b/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp @@ -209,8 +209,8 @@ FunctionBodyTransformerPass::run(Function &F, FunctionAnalysisManager &FAM) { // (As it uses currently unsupported instructions). We generate an // requires false; - contract instead. if (F.getName().str() == constants::SWIFT_FATAL_ERROR) { - ErrorReporter::addWarning( - SOURCE_LOC, "Skipping body of swift fatalError", F); + ErrorReporter::addWarning(SOURCE_LOC, + "Skipping body of swift fatalError", F); return PreservedAnalyses::all(); } diff --git a/src/llvm/lib/Passes/Function/FunctionContractDeclarer.cpp b/src/llvm/lib/Passes/Function/FunctionContractDeclarer.cpp index bd0b792bb..1d17c4358 100644 --- a/src/llvm/lib/Passes/Function/FunctionContractDeclarer.cpp +++ b/src/llvm/lib/Passes/Function/FunctionContractDeclarer.cpp @@ -50,11 +50,11 @@ FunctionContractDeclarerPass::run(Function &F, FunctionAnalysisManager &FAM) { colContract->set_allocated_blame(new col::Blame()); colContract->set_name(F.getName()); - // Add a "requires false"-contract to Swift's fatalError-function + // Add a "requires false"-contract to Swift's fatalError-function // (Since we currently do not support all instructions that it uses). if (F.getName().str() == constants::SWIFT_FATAL_ERROR) { - ErrorReporter::addWarning( - SOURCE_LOC, "Generating contract forswift fatalError", F); + ErrorReporter::addWarning(SOURCE_LOC, + "Generating contract forswift fatalError", F); colContract->set_value("requires false;"); colContract->set_allocated_origin( llvm2col::generateFunctionContractOrigin(F, "requires false;")); diff --git a/src/llvm/lib/Transform/Instruction/IntrinsicsTransform.cpp b/src/llvm/lib/Transform/Instruction/IntrinsicsTransform.cpp index c11eecccf..87dc2b446 100644 --- a/src/llvm/lib/Transform/Instruction/IntrinsicsTransform.cpp +++ b/src/llvm/lib/Transform/Instruction/IntrinsicsTransform.cpp @@ -44,6 +44,10 @@ void llvm2col::transformIntrinsic(llvm::CallInst &callInstruction, case llvm::Intrinsic::dbg_assign: // Ignore debug-intrinsics break; + case llvm::Intrinsic::lifetime_start: + case llvm::Intrinsic::lifetime_end: + // Ignore lifetime intrinsics + break; default: reportUnsupportedOperatorError(SOURCE_LOC, callInstruction); } From 3bcc3e6d3a0f25992aec4ef7c0c55036abc77e2a Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Tue, 25 Feb 2025 16:36:27 +0100 Subject: [PATCH 08/14] Pallas: Encode xor %1 true as not %1, Skip unused global --- .../Transform/Instruction/BinaryOpTransform.h | 4 ++ src/llvm/include/Transform/Transform.h | 15 ++++++ .../Passes/Module/GlobalVariableDeclarer.cpp | 22 ++++---- .../Instruction/BinaryOpTransform.cpp | 50 +++++++++++++++++-- 4 files changed, 74 insertions(+), 17 deletions(-) diff --git a/src/llvm/include/Transform/Instruction/BinaryOpTransform.h b/src/llvm/include/Transform/Instruction/BinaryOpTransform.h index e9ee68874..170e4f6e8 100644 --- a/src/llvm/include/Transform/Instruction/BinaryOpTransform.h +++ b/src/llvm/include/Transform/Instruction/BinaryOpTransform.h @@ -10,5 +10,9 @@ void transformBinaryOp(llvm::Instruction &llvmInstruction, col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); +void transformBitwiseXor(llvm::Instruction &llvmInstruction, + col::Assign &assignment, + pallas::FunctionCursor &funcCursor); + } // namespace llvm2col #endif // PALLAS_BINARYOPTRANSFORM_H diff --git a/src/llvm/include/Transform/Transform.h b/src/llvm/include/Transform/Transform.h index 4506aa4a9..c32d928dc 100644 --- a/src/llvm/include/Transform/Transform.h +++ b/src/llvm/include/Transform/Transform.h @@ -1,6 +1,9 @@ #ifndef PALLAS_TRANSFORM_H #define PALLAS_TRANSFORM_H +#include +#include + #include "Origin/OriginProvider.h" #include "Passes/Function/FunctionBodyTransformer.h" @@ -70,6 +73,18 @@ void transformBinExpr(llvm::Instruction &llvmInstruction, llvm2col::transformAndSetExpr(funcCursor, llvmInstruction, *llvmInstruction.getOperand(1), *rExpr); } +template +void transformBitwiseBinExpr(llvm::Instruction &llvmInstruction, + ColBinBitExpr &colBinBitExpr, + pallas::FunctionCursor &funcCursor) { + llvm::IntegerType *ty = + llvm::cast(llvmInstruction.getType()); + transformBinExpr(llvmInstruction, colBinBitExpr, funcCursor); + colBinBitExpr.set_allocated_blame(new col::Blame()); + colBinBitExpr.set_bits(ty->getBitWidth()); + colBinBitExpr.set_signed_(true); + // TODO: Figure out what to put for signed +} template int64_t setColNodeId(IDNode &idNode) { auto id = reinterpret_cast(idNode); diff --git a/src/llvm/lib/Passes/Module/GlobalVariableDeclarer.cpp b/src/llvm/lib/Passes/Module/GlobalVariableDeclarer.cpp index bbfd56cea..b8053bdc8 100644 --- a/src/llvm/lib/Passes/Module/GlobalVariableDeclarer.cpp +++ b/src/llvm/lib/Passes/Module/GlobalVariableDeclarer.cpp @@ -13,11 +13,6 @@ PreservedAnalyses GlobalVariableDeclarerPass::run(Module &M, auto pProgram = MAM.getResult(M).program; for (auto &global : M.globals()) { - // Skip the entry-point global from swift, as it contains currently - // unsupported poitner-casting and is not needed for verification. - if (global.getSection().str() == constants::SWIFT_ENTRY_SECTION) - continue; - col::GlobalDeclaration *globDecl = pProgram->add_declarations(); col::LlvmGlobalVariable *colGlobal = globDecl->mutable_llvm_global_variable(); @@ -25,13 +20,16 @@ PreservedAnalyses GlobalVariableDeclarerPass::run(Module &M, llvm2col::transformAndSetType(*global.getType(), *colGlobal->mutable_variable_type()); if (global.hasInitializer()) { - llvm2col::transformAndSetConstExpr( - MAM.getResult(M) - .getManager(), - llvm2col::generateGlobalVariableInitializerOrigin( - M, global, *global.getInitializer()), - *global.getInitializer(), *colGlobal->mutable_value()); - + // Skip the entry-point global from swift, as it contains currently + // unsupported poitner-casting and is not needed for verification. + if (global.getSection().str() != constants::SWIFT_ENTRY_SECTION) { + llvm2col::transformAndSetConstExpr( + MAM.getResult(M) + .getManager(), + llvm2col::generateGlobalVariableInitializerOrigin( + M, global, *global.getInitializer()), + *global.getInitializer(), *colGlobal->mutable_value()); + } llvm2col::transformAndSetType(*global.getInitializer()->getType(), *colGlobal->mutable_variable_type()); } else { diff --git a/src/llvm/lib/Transform/Instruction/BinaryOpTransform.cpp b/src/llvm/lib/Transform/Instruction/BinaryOpTransform.cpp index dbaa56af6..d2af24a4b 100644 --- a/src/llvm/lib/Transform/Instruction/BinaryOpTransform.cpp +++ b/src/llvm/lib/Transform/Instruction/BinaryOpTransform.cpp @@ -5,6 +5,9 @@ #include "Transform/Transform.h" #include "Util/Exceptions.h" +#include +#include + const std::string SOURCE_LOC = "Transform::Instruction::BinaryOp"; void llvm2col::transformBinaryOp(llvm::Instruction &llvmInstruction, @@ -51,34 +54,71 @@ void llvm2col::transformBinaryOp(llvm::Instruction &llvmInstruction, case llvm::Instruction::And: { col::BitAnd &expr = *assignment.mutable_value()->mutable_bit_and(); transformBinExpr(llvmInstruction, expr, funcCursor); + expr.set_allocated_blame(new col::Blame()); break; } case llvm::Instruction::Or: { col::BitOr &expr = *assignment.mutable_value()->mutable_bit_or(); - transformBinExpr(llvmInstruction, expr, funcCursor); + transformBitwiseBinExpr(llvmInstruction, expr, funcCursor); break; } case llvm::Instruction::Xor: { - col::BitXor &expr = *assignment.mutable_value()->mutable_bit_xor(); - transformBinExpr(llvmInstruction, expr, funcCursor); + transformBitwiseXor(llvmInstruction, assignment, funcCursor); break; } case llvm::Instruction::Shl: { col::BitShl &expr = *assignment.mutable_value()->mutable_bit_shl(); - transformBinExpr(llvmInstruction, expr, funcCursor); + transformBitwiseBinExpr(llvmInstruction, expr, funcCursor); break; } case llvm::Instruction::LShr: { col::BitUShr &expr = *assignment.mutable_value()->mutable_bit_u_shr(); - transformBinExpr(llvmInstruction, expr, funcCursor); + transformBitwiseBinExpr(llvmInstruction, expr, funcCursor); break; } case llvm::Instruction::AShr: { + llvm::IntegerType *ty = + llvm::cast(llvmInstruction.getType()); col::BitShr &expr = *assignment.mutable_value()->mutable_bit_shr(); transformBinExpr(llvmInstruction, expr, funcCursor); + expr.set_allocated_blame(new col::Blame()); + expr.set_bits(ty->getBitWidth()); break; } default: reportUnsupportedOperatorError(SOURCE_LOC, llvmInstruction); } } + +void llvm2col::transformBitwiseXor(llvm::Instruction &llvmInstruction, + col::Assign &assignment, + pallas::FunctionCursor &funcCursor) { + // We encode some common cases manually, to avoid having to use bitvectors. + llvm::Type *ty = llvmInstruction.getType(); + if (llvmInstruction.getType()->isIntegerTy(1)) { + // Binary operation on booleans + auto *rightAsConst = llvm::dyn_cast_if_present( + llvmInstruction.getOperand(1)); + if (rightAsConst != nullptr && rightAsConst->isOne()) { + // XOR %1 true --> not %1 + col::Not *colNot = assignment.mutable_value()->mutable_not_(); + colNot->set_allocated_origin(generateBinExprOrigin(llvmInstruction)); + llvm2col::transformAndSetExpr(funcCursor, llvmInstruction, + *llvmInstruction.getOperand(0), *colNot->mutable_arg()); + return; + } + auto *leftAsConst = llvm::dyn_cast_if_present( + llvmInstruction.getOperand(0)); + if (leftAsConst != nullptr && leftAsConst->isOne()) { + // XOR true %2 --> not %2 + col::Not *colNot = assignment.mutable_value()->mutable_not_(); + colNot->set_allocated_origin(generateBinExprOrigin(llvmInstruction)); + llvm2col::transformAndSetExpr(funcCursor, llvmInstruction, + *llvmInstruction.getOperand(1), *colNot->mutable_arg()); + return; + } + } + + col::BitXor &expr = *assignment.mutable_value()->mutable_bit_xor(); + transformBitwiseBinExpr(llvmInstruction, expr, funcCursor); +} \ No newline at end of file From 18d9c839a761465e079ccf838258c3f6d2c20f0a Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Wed, 26 Feb 2025 17:06:56 +0100 Subject: [PATCH 09/14] Pallas: encode bitwise xor with constant, add casts for handle trivial struct-pointers, support global int constants --- .../vct/col/typerules/CoercingRewriter.scala | 5 ++ .../Instruction/IntrinsicsTransform.h | 7 ++ .../include/Transform/LoopContractTransform.h | 8 +++ .../Instruction/BinaryOpTransform.cpp | 12 ++-- .../lib/Transform/LoopContractTransform.cpp | 64 +++++++++++++++---- .../vct/rewrite/lang/LangLLVMToCol.scala | 23 +++++-- 6 files changed, 96 insertions(+), 23 deletions(-) diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala index 0f502e95e..e23c9817e 100644 --- a/src/col/vct/col/typerules/CoercingRewriter.scala +++ b/src/col/vct/col/typerules/CoercingRewriter.scala @@ -2212,6 +2212,7 @@ abstract class CoercingRewriter[Pre <: Generation]() case LLVMForall(_, _) => e case LLVMSepForall(_, _) => e case LLVMExists(_, _) => e + case LLVMExtractValue(_, _, _, _) => e case PVLEndpointExpr(_, _) => e case EndpointExpr(ref, expr) => e case ChorExpr(expr) => ChorExpr(bool(expr)) @@ -2330,6 +2331,10 @@ abstract class CoercingRewriter[Pre <: Generation]() LLVMStore(value, p, ordering)(store.blame) case fracOf: LLVMFracOf[Pre] => fracOf case unreachable: LLVMBranchUnreachable[Pre] => unreachable + case add: LLVMAddWithOverflow[Pre] => add + case sub: LLVMSubWithOverflow[Pre] => sub + case mult: LLVMMultWithOverflow[Pre] => mult + case memset: LLVMMemset[Pre] => memset case ModelDo(model, perm, after, action, impl) => ModelDo(model, rat(perm), after, action, impl) case n @ Notify(obj) => Notify(cls(obj))(n.blame) diff --git a/src/llvm/include/Transform/Instruction/IntrinsicsTransform.h b/src/llvm/include/Transform/Instruction/IntrinsicsTransform.h index 0f20efb98..49abe0a86 100644 --- a/src/llvm/include/Transform/Instruction/IntrinsicsTransform.h +++ b/src/llvm/include/Transform/Instruction/IntrinsicsTransform.h @@ -49,6 +49,13 @@ void transformMultWithOverflow(llvm::CallInst &callInstruction, col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor, bool sign); +/** + * Transform call to the @llvm.memset.*-intrinsic + */ +void transformMemset(llvm::CallInst &callInstruction, + col::LlvmBasicBlock &colBlock, + pallas::FunctionCursor &funcCursor); + } // namespace llvm2col #endif // PALLAS_INTRINSICSTRANSFORM_H diff --git a/src/llvm/include/Transform/LoopContractTransform.h b/src/llvm/include/Transform/LoopContractTransform.h index cef923608..95d4041e9 100644 --- a/src/llvm/include/Transform/LoopContractTransform.h +++ b/src/llvm/include/Transform/LoopContractTransform.h @@ -24,6 +24,14 @@ bool addInvariantToContract(llvm::MDNode &invMD, llvm::Loop &llvmLoop, llvm::MDNode &contractLoc, pallas::FunctionCursor &functionCursor); +/** + * Build argument-expression that dereferences the value of the given alloca. + */ +void buildArgExprFromAlloca(col::LlvmFunctionInvocation &wrapperCall, + unsigned int argIdx, llvm::AllocaInst &llvmAlloca, + llvm::Function &llvmWFunc, llvm::MDNode &srcLoc, + pallas::FunctionCursor &functionCursor); + } // namespace llvm2col #endif // PALLAS_LOOPCONTRACTTRANSFORM_H \ No newline at end of file diff --git a/src/llvm/lib/Transform/Instruction/BinaryOpTransform.cpp b/src/llvm/lib/Transform/Instruction/BinaryOpTransform.cpp index d2af24a4b..2e462d110 100644 --- a/src/llvm/lib/Transform/Instruction/BinaryOpTransform.cpp +++ b/src/llvm/lib/Transform/Instruction/BinaryOpTransform.cpp @@ -102,9 +102,11 @@ void llvm2col::transformBitwiseXor(llvm::Instruction &llvmInstruction, if (rightAsConst != nullptr && rightAsConst->isOne()) { // XOR %1 true --> not %1 col::Not *colNot = assignment.mutable_value()->mutable_not_(); - colNot->set_allocated_origin(generateBinExprOrigin(llvmInstruction)); + colNot->set_allocated_origin( + generateBinExprOrigin(llvmInstruction)); llvm2col::transformAndSetExpr(funcCursor, llvmInstruction, - *llvmInstruction.getOperand(0), *colNot->mutable_arg()); + *llvmInstruction.getOperand(0), + *colNot->mutable_arg()); return; } auto *leftAsConst = llvm::dyn_cast_if_present( @@ -112,9 +114,11 @@ void llvm2col::transformBitwiseXor(llvm::Instruction &llvmInstruction, if (leftAsConst != nullptr && leftAsConst->isOne()) { // XOR true %2 --> not %2 col::Not *colNot = assignment.mutable_value()->mutable_not_(); - colNot->set_allocated_origin(generateBinExprOrigin(llvmInstruction)); + colNot->set_allocated_origin( + generateBinExprOrigin(llvmInstruction)); llvm2col::transformAndSetExpr(funcCursor, llvmInstruction, - *llvmInstruction.getOperand(1), *colNot->mutable_arg()); + *llvmInstruction.getOperand(1), + *colNot->mutable_arg()); return; } } diff --git a/src/llvm/lib/Transform/LoopContractTransform.cpp b/src/llvm/lib/Transform/LoopContractTransform.cpp index 2b999760a..61668c301 100644 --- a/src/llvm/lib/Transform/LoopContractTransform.cpp +++ b/src/llvm/lib/Transform/LoopContractTransform.cpp @@ -1,4 +1,5 @@ #include "Transform/LoopContractTransform.h" +#include "Transform/Transform.h" #include "Origin/OriginProvider.h" #include "Passes/Function/FunctionDeclarer.h" #include "Util/Constants.h" @@ -9,6 +10,7 @@ #include #include #include +#include #include #include #include @@ -147,7 +149,7 @@ bool llvm2col::addInvariantToContract(llvm::MDNode &invMD, llvm::Loop &llvmLoop, wrapperCall->mutable_ref()->set_id(colWFunc.id()); // Add arguments to wrapper-call - for (auto *diVar : diVars) { + for (auto [argIdx, diVar] : llvm::enumerate(diVars)) { // Match DIVariables to LLVM-Values llvm::Value *llvmVal = pallas::utils::mapDIVarToValue(*llvmParentFunc, *diVar, &llvmLoop); @@ -160,17 +162,9 @@ bool llvm2col::addInvariantToContract(llvm::MDNode &invMD, llvm::Loop &llvmLoop, // Get variables from llvm-values and build argument-expressions if (llvm::isa(llvmVal)) { - col::Variable *colVar = - &functionCursor.getVariableMapEntry(*llvmVal, false); - auto *ptrDeref = wrapperCall->add_args()->mutable_deref_pointer(); - ptrDeref->set_allocated_origin( - llvm2col::generatePallasWrapperCallOrigin(*llvmWFunc, *srcLoc)); - ptrDeref->set_allocated_blame(new col::Blame()); - // Local to var of alloca - auto *local = ptrDeref->mutable_pointer()->mutable_local(); - local->set_allocated_origin( - llvm2col::generatePallasWrapperCallOrigin(*llvmWFunc, *srcLoc)); - local->mutable_ref()->set_id(colVar->id()); + llvm2col::buildArgExprFromAlloca( + *wrapperCall, argIdx, *llvm::cast(llvmVal), + *llvmWFunc, *srcLoc, functionCursor); } else if (llvm::isa(llvmVal)) { col::Variable *colVar = &functionCursor.getVariableMapEntry(*llvmVal, true); @@ -218,4 +212,50 @@ void llvm2col::initializeEmptyLoopContract(col::LoopContract &colContract) { tt->set_allocated_origin(generateLabelledOrigin("constant true")); invariant->set_allocated_origin(generateLabelledOrigin("constant true")); invariant->mutable_blame(); +} + +void llvm2col::buildArgExprFromAlloca(col::LlvmFunctionInvocation &wrapperCall, + unsigned int argIdx, + llvm::AllocaInst &llvmAlloca, + llvm::Function &llvmWFunc, + llvm::MDNode &srcLoc, + pallas::FunctionCursor &functionCursor) { + col::Variable &colVar = + functionCursor.getVariableMapEntry(llvmAlloca, false); + // Ptr deref + auto *ptrDeref = wrapperCall.add_args()->mutable_deref_pointer(); + ptrDeref->set_allocated_origin( + llvm2col::generatePallasWrapperCallOrigin(llvmWFunc, srcLoc)); + ptrDeref->set_allocated_blame(new col::Blame()); + + // Cast, if type is packed struct with single element + auto *structTy = + llvm::dyn_cast(llvmAlloca.getAllocatedType()); + llvm::Type *expectedTy = llvmWFunc.getArg(argIdx)->getType(); + bool isTrivialStruct = structTy != nullptr && structTy->isPacked() && + structTy->getNumElements() == 1; + + col::Local *local = nullptr; + if (structTy != expectedTy && isTrivialStruct && + structTy->getElementType(0) == expectedTy) { + auto *cast = ptrDeref->mutable_pointer()->mutable_cast(); + cast->set_allocated_origin( + llvm2col::generatePallasWrapperCallOrigin(llvmWFunc, srcLoc)); + col::TypeValue *tVal = cast->mutable_type_value()->mutable_type_value(); + tVal->set_allocated_origin( + llvm2col::generatePallasWrapperCallOrigin(llvmWFunc, srcLoc)); + // TODO: Set correct type for cast (i.e. is missing a pointer) + llvm2col::transformAndSetPointerType(*expectedTy, *tVal->mutable_value()); + // llvm2col::transformAndSetType(*expectedTy, *tVal->mutable_value()); + // tVal->set_allocated_value(); + // llvm2col::transformAndSetType(*expectedTy, *tVal->mutable_value()); + local = cast->mutable_value()->mutable_local(); + } else { + local = ptrDeref->mutable_pointer()->mutable_local(); + } + + // Local to var of alloca + local->set_allocated_origin( + llvm2col::generatePallasWrapperCallOrigin(llvmWFunc, srcLoc)); + local->mutable_ref()->set_id(colVar.id()); } \ No newline at end of file diff --git a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala index 4ee064f7d..c1535f44b 100644 --- a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala @@ -678,7 +678,7 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) // TODO: Handle the initializer // TODO: Include array and vector bounds somehow globalVariableInferredType.getOrElse(decl, decl.variableType) match { - case struct: LLVMTStruct[Pre] => { + case struct: LLVMTStruct[Pre] => rewriteStruct(struct) globalVariableMap.update( decl, @@ -693,8 +693,7 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) )(decl.o) ), ) - } - case array: LLVMTArray[Pre] => { + case array: LLVMTArray[Pre] => globalVariableMap.update( decl, rw.globalDeclarations.declare( @@ -703,8 +702,7 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) )(decl.o) ), ) - } - case vector: LLVMTVector[Pre] => { + case vector: LLVMTVector[Pre] => globalVariableMap.update( decl, rw.globalDeclarations.declare( @@ -713,8 +711,13 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) )(decl.o) ), ) - } - case _ => { ??? } + case int: LLVMTInt[Pre] => + globalVariableMap.update( + decl, + rw.globalDeclarations + .declare(new HeapVariable[Post](rw.dispatch(int))(decl.o)), + ) + case _ => ??? } } @@ -994,6 +997,7 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) case _ => ??? // Should never happen } // Assign new object to target + if (!structMap.contains(targetStructT)) { rewriteStruct(targetStructT) } val newCls = structMap.get(targetStructT).get val assignNew = Assign(rw.dispatch(instr.target), new NewObject[Post](newCls.ref))( @@ -1467,6 +1471,10 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) buildPhiAssignments(bb), eliminate(branch), )) + case unr: LLVMBranchUnreachable[Pre] => + Block[Post]( + Seq(rw.dispatch(bb.body), buildPhiAssignments(bb), rw.dispatch(unr)) + ) case other => throw UnexpectedLLVMNode(other) } } @@ -1492,6 +1500,7 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) } def structType(t: LLVMTStruct[Pre]): Type[Post] = { + if (!structMap.contains(t)) { rewriteStruct(t) } val targetClass = new LazyRef[Post, Class[Post]](structMap(t)) TByValueClass[Post](targetClass, Seq())(t.o) } From a01d95968f4d62aaff307fec0ca239b6b640c2f4 Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Wed, 26 Feb 2025 17:26:30 +0100 Subject: [PATCH 10/14] Pallas: Added node for memset intrinsic --- src/col/vct/col/ast/Node.scala | 8 +++++ .../col/ast/lang/llvm/LLVMMemsetImpl.scala | 14 +++++++++ .../Instruction/IntrinsicsTransform.cpp | 31 +++++++++++++++++++ .../lib/Transform/LoopContractTransform.cpp | 5 +-- 4 files changed, 56 insertions(+), 2 deletions(-) create mode 100644 src/col/vct/col/ast/lang/llvm/LLVMMemsetImpl.scala diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index cfa952d56..32bd94cfe 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -3754,6 +3754,14 @@ final case class LLVMStore[G]( )(val blame: Blame[VerificationFailure])(implicit val o: Origin) extends LLVMStatement[G] with LLVMStoreImpl[G] +final case class LLVMMemset[G]( + dest: Expr[G], + value: Expr[G], + len: Expr[G], + volatile: Expr[G], +)(val blame: Blame[VerificationFailure])(implicit val o: Origin) + extends LLVMStatement[G] with LLVMMemsetImpl[G] + final case class LLVMBranchUnreachable[G]()( val blame: Blame[UnreachableReachedError] )(implicit val o: Origin) diff --git a/src/col/vct/col/ast/lang/llvm/LLVMMemsetImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMMemsetImpl.scala new file mode 100644 index 000000000..f4434b265 --- /dev/null +++ b/src/col/vct/col/ast/lang/llvm/LLVMMemsetImpl.scala @@ -0,0 +1,14 @@ +package vct.col.ast.lang.llvm + +import vct.col.ast.LLVMMemset +import vct.col.ast.ops.LLVMMemsetOps +import vct.col.print.{Text, _} + +trait LLVMMemsetImpl[G] extends LLVMMemsetOps[G] { + this: LLVMMemset[G] => + + override def layout(implicit ctx: Ctx): Doc = { + Text("memset(") <+> dest.show <+> Text(", ") <+> value.show <+> + Text(", ") <+> len.show <+> Text(", ") <+> volatile.show <+> Text(")") + } +} diff --git a/src/llvm/lib/Transform/Instruction/IntrinsicsTransform.cpp b/src/llvm/lib/Transform/Instruction/IntrinsicsTransform.cpp index 87dc2b446..36226dfa5 100644 --- a/src/llvm/lib/Transform/Instruction/IntrinsicsTransform.cpp +++ b/src/llvm/lib/Transform/Instruction/IntrinsicsTransform.cpp @@ -48,6 +48,9 @@ void llvm2col::transformIntrinsic(llvm::CallInst &callInstruction, case llvm::Intrinsic::lifetime_end: // Ignore lifetime intrinsics break; + case llvm::Intrinsic::memset: + transformMemset(callInstruction, colBlock, funcCursor); + break; default: reportUnsupportedOperatorError(SOURCE_LOC, callInstruction); } @@ -168,3 +171,31 @@ void llvm2col::transformMultWithOverflow(llvm::CallInst &callInstruction, *callInstruction.getArgOperand(1), *mult->mutable_right()); } + +void llvm2col::transformMemset(llvm::CallInst &callInstruction, + col::LlvmBasicBlock &colBlock, + pallas::FunctionCursor &funcCursor) { + llvm::Function *intrFunc = callInstruction.getCalledFunction(); + col::Block &body = pallas::bodyAsBlock(colBlock); + col::Variable &targetVar = funcCursor.declareVariable(callInstruction); + col::LlvmMemset *memset = body.add_statements()->mutable_llvm_memset(); + memset->set_allocated_origin( + llvm2col::generateSingleStatementOrigin(callInstruction)); + memset->set_allocated_blame(new col::Blame()); + // dest + llvm2col::transformAndSetExpr(funcCursor, callInstruction, + *callInstruction.getArgOperand(0), + *memset->mutable_dest()); + // value + llvm2col::transformAndSetExpr(funcCursor, callInstruction, + *callInstruction.getArgOperand(1), + *memset->mutable_value()); + // len + llvm2col::transformAndSetExpr(funcCursor, callInstruction, + *callInstruction.getArgOperand(2), + *memset->mutable_len()); + // volatile + llvm2col::transformAndSetExpr(funcCursor, callInstruction, + *callInstruction.getArgOperand(3), + *memset->mutable_volatile_()); +} diff --git a/src/llvm/lib/Transform/LoopContractTransform.cpp b/src/llvm/lib/Transform/LoopContractTransform.cpp index 61668c301..bf18f1598 100644 --- a/src/llvm/lib/Transform/LoopContractTransform.cpp +++ b/src/llvm/lib/Transform/LoopContractTransform.cpp @@ -1,7 +1,7 @@ #include "Transform/LoopContractTransform.h" -#include "Transform/Transform.h" #include "Origin/OriginProvider.h" #include "Passes/Function/FunctionDeclarer.h" +#include "Transform/Transform.h" #include "Util/Constants.h" #include "Util/Exceptions.h" #include "Util/PallasDIMapping.h" @@ -245,7 +245,8 @@ void llvm2col::buildArgExprFromAlloca(col::LlvmFunctionInvocation &wrapperCall, tVal->set_allocated_origin( llvm2col::generatePallasWrapperCallOrigin(llvmWFunc, srcLoc)); // TODO: Set correct type for cast (i.e. is missing a pointer) - llvm2col::transformAndSetPointerType(*expectedTy, *tVal->mutable_value()); + llvm2col::transformAndSetPointerType(*expectedTy, + *tVal->mutable_value()); // llvm2col::transformAndSetType(*expectedTy, *tVal->mutable_value()); // tVal->set_allocated_value(); // llvm2col::transformAndSetType(*expectedTy, *tVal->mutable_value()); From cd8ef7872ebda880058b5d1cfc4c4e0ab205350d Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Thu, 27 Feb 2025 10:55:20 +0100 Subject: [PATCH 11/14] Pallas: Change encoding of arithmetic-intrinsics with overflow to using initializer functions --- .../vct/rewrite/lang/LangLLVMToCol.scala | 90 +++++++++++++------ 1 file changed, 62 insertions(+), 28 deletions(-) diff --git a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala index c1535f44b..e459f7ddc 100644 --- a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala @@ -93,6 +93,11 @@ case object LangLLVMToCol { LabelContext("Generated context for resArg"), )) + private val overflowOpInitializerOrigin: Origin = Origin(Seq( + PreferredName(Seq("initStruct")), + LabelContext("Generated initializer for arith-op with overflow"), + )) + // TODO: This should be replaced with the correct blames! private object InvalidGEP extends PanicBlame("Invalid use of getelementpointer!") @@ -148,6 +153,11 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) private val assignedInLoop: ScopedStack[mutable.Set[Variable[Pre]]] = ScopedStack() + // Initializer-functions for the structs that are returned by the llvm intrinsics + // for arithmetic operaitons with overflows. + private val overflowOpInitializers + : mutable.Map[LLVMTStruct[Pre], Procedure[Post]] = mutable.Map() + def gatherPallasTypeSubst(program: Program[Pre]): Unit = { // Get all variables that are assigned a new type directly program.collect { @@ -985,10 +995,53 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) CastFloat(rw.dispatch(fpext.value), rw.dispatch(fpext.t)) } + private def getInitializerForArithOpWithOverflow( + resT: LLVMTStruct[Pre] + ): Procedure[Post] = { + if (!overflowOpInitializers.contains(resT)) { + implicit val o: Origin = overflowOpInitializerOrigin + val derefByValBlame = PanicBlame("By-value type always has permission") + val resArg = + new Variable[Post](rw.dispatch(resT.elements(0)))( + o.where(name = "resArg") + ) + val flagArg = + new Variable[Post](rw.dispatch(resT.elements(1)))( + o.where(name = "flagArg") + ) + val resField = structFieldMap((resT, 0)) + val flagField = structFieldMap((resT, 1)) + + val initializer = rw.globalDeclarations.declare { + withResult((result: Result[Post]) => { + new Procedure[Post]( + returnType = rw.dispatch(resT), + args = Seq(resArg, flagArg), + outArgs = Nil, + typeArgs = Nil, + body = None, + contract = contract[Post]( + blame = PanicBlame("Generated contract cannot fail"), + ensures = UnitAccountedPredicate( + (Deref[Post](result, resField.ref)(derefByValBlame) === + Local(resArg.ref)) && + (Deref[Post](result, flagField.ref)(derefByValBlame) === + Local(flagArg.ref)) + ), + ), + pure = true, + )(PanicBlame("Generated initializer does not raise errors")) + }) + } + overflowOpInitializers(resT) = initializer + } + overflowOpInitializers(resT) + } + private def rewriteArithOpWithOverflow( instr: LLVMArithOpWithOverflow[Pre], op: (Expr[Post], Expr[Post]) => Expr[Post], - ) = { + ): Statement[Post] = { implicit val o: Origin = instr.o // TODO: Do not ignore the signedness val targetStructT = @@ -998,33 +1051,14 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) } // Assign new object to target if (!structMap.contains(targetStructT)) { rewriteStruct(targetStructT) } - val newCls = structMap.get(targetStructT).get - val assignNew = - Assign(rw.dispatch(instr.target), new NewObject[Post](newCls.ref))( - instr.blame - ) - // Set result-field - val resField = structFieldMap((targetStructT, 0)) - val assignRes = - Assign( - Deref[Post](rw.dispatch(instr.target), resField.ref)(PanicBlame( - "Generated object always has permissions" - )), - op(rw.dispatch(instr.left), rw.dispatch(instr.right)), - )(instr.blame) - - // Set overflow-flag - val flagField = structFieldMap((targetStructT, 1)) - val assignFlag = - Assign( - Deref[Post](rw.dispatch(instr.target), flagField.ref)(PanicBlame( - "Generated object always has permissions" - )), - ff, - )(instr.blame) - - // Build Block - Block(Seq(assignNew, assignRes, assignFlag)) + val initFunc = getInitializerForArithOpWithOverflow(targetStructT) + val initCall = procedureInvocation[Post]( + blame = PanicBlame("Generated initializer does not fail"), + ref = initFunc.ref, + args = Seq(op(rw.dispatch(instr.left), rw.dispatch(instr.right)), ff), + ) + val assign = Assign(rw.dispatch(instr.target), initCall)(instr.blame) + assign } def rewriteAddWithOverflow(add: LLVMAddWithOverflow[Pre]): Statement[Post] = { From b60c9a79f5c0eeff65f992f9b3b106bc733e5416 Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Thu, 27 Feb 2025 13:02:06 +0100 Subject: [PATCH 12/14] Pallas: Fix failing tests --- src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala index e459f7ddc..49a4fb09b 100644 --- a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala @@ -1534,7 +1534,12 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) } def structType(t: LLVMTStruct[Pre]): Type[Post] = { - if (!structMap.contains(t)) { rewriteStruct(t) } + // TODO: Remove this. The check for the golbalDeclarations is required because + // the function-type is called in the post-comparisson in derefUntil, outside of + // a scope. Once that is removed, this should no longe be required. + if (!rw.globalDeclarations.isEmpty) { // <-- + if (!structMap.contains(t)) { rewriteStruct(t) } + } val targetClass = new LazyRef[Post, Class[Post]](structMap(t)) TByValueClass[Post](targetClass, Seq())(t.o) } From 14a1b4f71ad3c6f46ca32f95178faee91610cd73 Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Thu, 27 Feb 2025 15:16:43 +0100 Subject: [PATCH 13/14] Pallas: Change encoding of unreachable, allow assert in statement-to-expression --- .../vct/col/util/StatementToExpression.scala | 9 +- .../vct/rewrite/lang/LangLLVMToCol.scala | 110 ++++++++++++------ 2 files changed, 80 insertions(+), 39 deletions(-) diff --git a/src/col/vct/col/util/StatementToExpression.scala b/src/col/vct/col/util/StatementToExpression.scala index a3efcbddd..9b2a92597 100644 --- a/src/col/vct/col/util/StatementToExpression.scala +++ b/src/col/vct/col/util/StatementToExpression.scala @@ -55,6 +55,13 @@ case class StatementToExpression[Pre <: Generation, Post <: Generation]( } } } + case a @ Assert(e) => + alt match { + case Some(exprAlt) => + Some(Asserting[Post](rw.dispatch(e), exprAlt)(a.blame)(a.o)) + case None => + throw errorBuilder("Assert may not be the last statement") + } case _ => None } } @@ -88,7 +95,7 @@ case class StatementToExpression[Pre <: Generation, Post <: Generation]( else 0 ) - case Assign(_, _) => None + case Assert(_) => Some(0) case _ => None } diff --git a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala index 49a4fb09b..8b3cbd61d 100644 --- a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala @@ -98,6 +98,11 @@ case object LangLLVMToCol { LabelContext("Generated initializer for arith-op with overflow"), )) + private val nondetValueOrigin: Origin = Origin(Seq( + LabelContext("Getter for nondeterministic value"), + PreferredName(Seq("getNondet")), + )) + // TODO: This should be replaced with the correct blames! private object InvalidGEP extends PanicBlame("Invalid use of getelementpointer!") @@ -158,6 +163,14 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) private val overflowOpInitializers : mutable.Map[LLVMTStruct[Pre], Procedure[Post]] = mutable.Map() + // Functions that are used to get a nondeterministic value of a given type. + // Used to encode the unreachable-instruction. + private val nondetGetters: mutable.Map[Type[Post], Function[Post]] = mutable + .Map() + + // Return type of the LLVMFunction that is currently rewritten + private val funcRetType: ScopedStack[Type[Post]] = ScopedStack() + def gatherPallasTypeSubst(program: Program[Pre]): Unit = { // Get all variables that are assigned a new type directly program.collect { @@ -495,43 +508,45 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) case None => None } val isWrapper = func.pallasExprWrapperFor.isDefined - rw.globalDeclarations.declare( - new Procedure[Post]( - returnType = - if (isWrapper) { TResource() } - else { - rw.dispatch(func.importedReturnType.getOrElse(func.returnType)) - }, - args = argList, - outArgs = Nil, - typeArgs = Nil, - body = - inWrapperFunction.having(isWrapper) { - func.functionBody match { - case None => None - case Some(functionBody) => - if (func.pure) - Some(GotoEliminator(functionBody match { - case scope: Scope[Pre] => scope; - case other => throw UnexpectedLLVMNode(other) - }).eliminate()) - else - Some(rw.dispatch(functionBody)) - } - }, - contract = - func.contract match { - case contract: VCLLVMFunctionContract[Pre] => - rw.dispatch(contract.data.get) - case contract: PallasFunctionContract[Pre] => - extendContractWithSretPerm(contract.content, cRetArg) - }, - pure = func.pure, - pallasWrapper = isWrapper, - pallasFunction = true, - )(func.blame) - ) - + val returnT = + if (isWrapper) { TResource[Post]() } + else { + rw.dispatch(func.importedReturnType.getOrElse(func.returnType)) + } + funcRetType.having(returnT) { + rw.globalDeclarations.declare( + new Procedure[Post]( + returnType = returnT, + args = argList, + outArgs = Nil, + typeArgs = Nil, + body = + inWrapperFunction.having(isWrapper) { + func.functionBody match { + case None => None + case Some(functionBody) => + if (func.pure) + Some(GotoEliminator(functionBody match { + case scope: Scope[Pre] => scope; + case other => throw UnexpectedLLVMNode(other) + }).eliminate()) + else + Some(rw.dispatch(functionBody)) + } + }, + contract = + func.contract match { + case contract: VCLLVMFunctionContract[Pre] => + rw.dispatch(contract.data.get) + case contract: PallasFunctionContract[Pre] => + extendContractWithSretPerm(contract.content, cRetArg) + }, + pure = func.pure, + pallasWrapper = isWrapper, + pallasFunction = true, + )(func.blame) + ) + } } } llvmFunctionMap.update(func, procedure) @@ -1082,7 +1097,26 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) unreachable: LLVMBranchUnreachable[Pre] ): Statement[Post] = { implicit val o: Origin = unreachable.o - Assert[Post](ff)(UnreachableReached(unreachable)) + val a = Assert[Post](ff)(UnreachableReached(unreachable)) + val nondetGetter = getNondetValFunc(funcRetType.top) + val r = Return[Post]( + functionInvocation[Post](blame = TrueSatisfiable, ref = nondetGetter.ref) + ) + Block(Seq(a, r)) + } + + private def getNondetValFunc(t: Type[Post]): Function[Post] = { + if (!nondetGetters.contains(t)) { + val getterFunc = rw.globalDeclarations.declare( + function[Post]( + blame = AbstractApplicable, + contractBlame = TrueSatisfiable, + returnType = t, + )(nondetValueOrigin) + ) + nondetGetters(t) = getterFunc + } + nondetGetters(t) } private def getInferredType(e: Expr[Pre]): Type[Pre] = From 474792552e20e9154f96ff602faa9e5aee2f8bb3 Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Thu, 27 Feb 2025 17:19:33 +0100 Subject: [PATCH 14/14] Pallas: Added (very) limited support for memset-intrinsic --- .../vct/rewrite/lang/LangLLVMToCol.scala | 59 +++++++++++++++++++ .../vct/rewrite/lang/LangSpecificToCol.scala | 1 + 2 files changed, 60 insertions(+) diff --git a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala index 8b3cbd61d..86f2c99d2 100644 --- a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala @@ -81,6 +81,14 @@ case object LangLLVMToCol { o.messageInContext(s"Unsupported aggregate-type used in extractvalue") } + private final case class UnsupportedMemset(memset: LLVMMemset[_]) + extends UserError { + override def code: String = "unsupportedMemset" + + override def text: String = + memset.o.messageInContext(s"Unsupported memset operation") + } + private final case class UnreachableReached( unreachable: LLVMBranchUnreachable[_] ) extends Blame[AssertFailed] { @@ -1250,6 +1258,57 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) } } + def rewriteMemset(memset: LLVMMemset[Pre]): Statement[Post] = { + implicit val o: Origin = memset.o + // Curently only memset with constant value of 0 is supported + memset.value match { + case LLVMIntegerValue(v, _) if v.intValue == 0 => + case _ => throw UnsupportedMemset(memset) + } + // TODO: Make this more more generic + // Currently, only very basic type-wrapper structs are supported (i.e. a packed struct with one integer value) + val numBytes = + memset.len match { + case LLVMIntegerValue(bytes, _) => bytes + case _ => throw UnsupportedMemset(memset) + } + val structType = + memset.dest match { + case Local(Ref(v)) => + v.t match { + case LLVMTPointer(Some(s: LLVMTStruct[Pre])) => s + case _ => throw throw UnsupportedMemset(memset) + } + case _ => throw UnsupportedMemset(memset) + } + if (!structType.packed || !(structType.elements.size == 1)) { + throw UnsupportedMemset(memset) + } + structType.elements.head match { + case LLVMTInt(bits) if (bits / 8) == numBytes => + case _ => throw UnsupportedMemset(memset) + } + + // Assign new value to the struct + val newCls = structMap.get(structType).get + val assignStruct = + Assign( + DerefPointer(rw.dispatch(memset.dest))(memset.blame), + new NewObject[Post](newCls.ref), + )(memset.blame) + // Set field of the struct to 0 + val structField = structFieldMap((structType, 0)) + val assignField = + Assign[Post]( + Deref[Post]( + DerefPointer(rw.dispatch(memset.dest))(memset.blame), + structField.ref, + )(memset.blame), + rw.dispatch(memset.value), + )(memset.blame) + Block(Seq(assignStruct, assignField)) + } + def rewritePointerValue(pointer: LLVMPointerValue[Pre]): Expr[Post] = { implicit val o: Origin = pointer.o // Will be transformed by VariableToPointer pass diff --git a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala index a87c0286f..34d522b19 100644 --- a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala @@ -335,6 +335,7 @@ case class LangSpecificToCol[Pre <: Generation]( case load: LLVMLoad[Pre] => llvm.rewriteLoad(load) case store: LLVMStore[Pre] => llvm.rewriteStore(store) case alloc: LLVMAllocA[Pre] => llvm.rewriteAllocA(alloc) + case memset: LLVMMemset[Pre] => llvm.rewriteMemset(memset) case block: LLVMBasicBlock[Pre] => llvm.rewriteBasicBlock(block) case unreachable: LLVMBranchUnreachable[Pre] => llvm.rewriteUnreachable(unreachable)