diff --git a/examples/concepts/llvm/pallas/pallas_c_fibonacci.c b/examples/concepts/llvm/pallas/pallas_c_fibonacci.c new file mode 100644 index 000000000..ae7fa5bbf --- /dev/null +++ b/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; +} \ No newline at end of file diff --git a/examples/concepts/llvm/pallas/pallas_c_fibonacci.ll b/examples/concepts/llvm/pallas/pallas_c_fibonacci.ll new file mode 100644 index 000000000..a53175ae4 --- /dev/null +++ b/examples/concepts/llvm/pallas/pallas_c_fibonacci.ll @@ -0,0 +1,309 @@ +; ModuleID = './tmp/tmp_ir_source0.ll' +source_filename = "examples/concepts/llvm/pallas/pallas_c_fibonacci.c" +target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128" +target triple = "x86_64-unknown-linux-gnu" + +@llvm.used = appending global [6 x ptr] [ptr @PALLAS_SPEC_2, ptr @PALLAS_SPEC_0, ptr @PALLAS_SPEC_1, ptr @PALLAS_SPEC_3, ptr @PALLAS_SPEC_4, ptr @PALLAS_SPEC_5], section "llvm.metadata" + +; Function Attrs: noinline nounwind uwtable +define dso_local i32 @fibRec(i32 noundef %0) #0 !dbg !12 !pallas.fcontract !17 { + call void @llvm.dbg.value(metadata i32 %0, metadata !21, metadata !DIExpression()), !dbg !22 + %2 = icmp eq i32 %0, 0, !dbg !23 + br i1 %2, label %3, label %4, !dbg !25 + +3: ; preds = %1 + br label %13, !dbg !26 + +4: ; preds = %1 + %5 = icmp eq i32 %0, 1, !dbg !28 + br i1 %5, label %6, label %7, !dbg !30 + +6: ; preds = %4 + br label %13, !dbg !31 + +7: ; preds = %4 + %8 = sub nsw i32 %0, 1, !dbg !33 + %9 = call i32 @fibRec(i32 noundef %8), !dbg !35 + %10 = sub nsw i32 %0, 2, !dbg !36 + %11 = call i32 @fibRec(i32 noundef %10), !dbg !37 + %12 = add nsw i32 %9, %11, !dbg !38 + br label %13, !dbg !39 + +13: ; preds = %7, %6, %3 + %.0 = phi i32 [ 0, %3 ], [ 1, %6 ], [ %12, %7 ], !dbg !40 + ret i32 %.0, !dbg !41 +} + +; Function Attrs: nocallback nofree nosync nounwind speculatable willreturn memory(none) +declare void @llvm.dbg.declare(metadata, metadata, metadata) #1 + +; Function Attrs: noinline nounwind uwtable +define dso_local i32 @fibIt(i32 noundef %0) #0 !dbg !42 !pallas.fcontract !43 { + call void @llvm.dbg.value(metadata i32 %0, metadata !47, metadata !DIExpression()), !dbg !50 + %2 = icmp eq i32 %0, 0, !dbg !51 + br i1 %2, label %3, label %4, !dbg !53 + +3: ; preds = %1 + br label %16, !dbg !54 + +4: ; preds = %1 + %5 = icmp eq i32 %0, 1, !dbg !56 + br i1 %5, label %6, label %7, !dbg !58 + +6: ; preds = %4 + br label %16, !dbg !59 + +7: ; preds = %4 + br label %8 + +8: ; preds = %7 + call void @llvm.dbg.value(metadata i32 0, metadata !61, metadata !DIExpression()), !dbg !50 + call void @llvm.dbg.value(metadata i32 1, metadata !62, metadata !DIExpression()), !dbg !50 + call void @llvm.dbg.value(metadata i32 2, metadata !63, metadata !DIExpression()), !dbg !65 + br label %9, !dbg !66 + +9: ; preds = %13, %8 + %.03 = phi i32 [ 1, %8 ], [ %12, %13 ], !dbg !50 + %.02 = phi i32 [ 0, %8 ], [ %.03, %13 ], !dbg !50 + %.01 = phi i32 [ 2, %8 ], [ %14, %13 ], !dbg !67 + call void @llvm.dbg.value(metadata i32 %.01, metadata !63, metadata !DIExpression()), !dbg !65 + call void @llvm.dbg.value(metadata i32 %.02, metadata !61, metadata !DIExpression()), !dbg !50 + call void @llvm.dbg.value(metadata i32 %.03, metadata !62, metadata !DIExpression()), !dbg !50 + %10 = icmp sle i32 %.01, %0, !dbg !68 + br i1 %10, label %11, label %15, !dbg !70 + +11: ; preds = %9 + %12 = add nsw i32 %.02, %.03, !dbg !71 + call void @llvm.dbg.value(metadata i32 %12, metadata !73, metadata !DIExpression()), !dbg !74 + call void @llvm.dbg.value(metadata i32 %.03, metadata !61, metadata !DIExpression()), !dbg !50 + call void @llvm.dbg.value(metadata i32 %12, metadata !62, metadata !DIExpression()), !dbg !50 + br label %13, !dbg !75 + +13: ; preds = %11 + %14 = add nsw i32 %.01, 1, !dbg !76 + call void @llvm.dbg.value(metadata i32 %14, metadata !63, metadata !DIExpression()), !dbg !65 + br label %9, !dbg !77, !llvm.loop !78 + +15: ; preds = %9 + br label %16, !dbg !89 + +16: ; preds = %15, %6, %3 + %.0 = phi i32 [ 0, %3 ], [ 1, %6 ], [ %.03, %15 ], !dbg !50 + ret i32 %.0, !dbg !90 +} + +; Function Attrs: nocallback nofree nosync nounwind speculatable willreturn memory(none) +declare void @llvm.dbg.value(metadata, metadata, metadata) #1 + +; Function Attrs: noinline nounwind uwtable +define dso_local zeroext i1 @PALLAS_SPEC_2(i32 noundef %0) #0 !dbg !91 !pallas.exprWrapper !95 { + call void @llvm.dbg.value(metadata i32 %0, metadata !96, metadata !DIExpression()), !dbg !97 + %2 = call i32 @pallas.result.0(), !dbg !98 + %3 = call i32 @fibRec(i32 noundef %0), !dbg !99 + %4 = icmp eq i32 %2, %3, !dbg !100 + ret i1 %4, !dbg !97 +} + +; Function Attrs: noinline nounwind uwtable +define dso_local zeroext i1 @PALLAS_SPEC_0(i32 noundef %0) #0 !dbg !101 !pallas.exprWrapper !95 { + call void @llvm.dbg.value(metadata i32 %0, metadata !102, metadata !DIExpression()), !dbg !103 + %2 = icmp sge i32 %0, 0, !dbg !104 + ret i1 %2, !dbg !103 +} + +; Function Attrs: noinline nounwind uwtable +define dso_local zeroext i1 @PALLAS_SPEC_1(i32 noundef %0) #0 !dbg !105 !pallas.exprWrapper !95 { + call void @llvm.dbg.value(metadata i32 %0, metadata !106, metadata !DIExpression()), !dbg !107 + %2 = icmp sge i32 %0, 0, !dbg !108 + ret i1 %2, !dbg !107 +} + +; Function Attrs: noinline nounwind uwtable +define dso_local zeroext i1 @PALLAS_SPEC_3(i32 noundef %0, i32 noundef %1, i32 noundef %2, i32 noundef %3) #0 !dbg !109 !pallas.exprWrapper !95 { + call void @llvm.dbg.value(metadata i32 %0, metadata !112, metadata !DIExpression()), !dbg !113 + call void @llvm.dbg.value(metadata i32 %1, metadata !114, metadata !DIExpression()), !dbg !113 + call void @llvm.dbg.value(metadata i32 %2, metadata !115, metadata !DIExpression()), !dbg !113 + call void @llvm.dbg.value(metadata i32 %3, metadata !116, metadata !DIExpression()), !dbg !113 + %5 = icmp sle i32 2, %3, !dbg !117 + %6 = add nsw i32 %0, 1, !dbg !118 + %7 = icmp sle i32 %3, %6, !dbg !119 + %8 = call i1 @pallas.scAnd(i1 %5, i1 %7), !dbg !120 + ret i1 %8, !dbg !113 +} + +; Function Attrs: noinline nounwind uwtable +define dso_local zeroext i1 @PALLAS_SPEC_4(i32 noundef %0, i32 noundef %1, i32 noundef %2, i32 noundef %3) #0 !dbg !121 !pallas.exprWrapper !95 { + call void @llvm.dbg.value(metadata i32 %0, metadata !122, metadata !DIExpression()), !dbg !123 + call void @llvm.dbg.value(metadata i32 %1, metadata !124, metadata !DIExpression()), !dbg !123 + call void @llvm.dbg.value(metadata i32 %2, metadata !125, metadata !DIExpression()), !dbg !123 + call void @llvm.dbg.value(metadata i32 %3, metadata !126, metadata !DIExpression()), !dbg !123 + %5 = sub nsw i32 %3, 1, !dbg !127 + %6 = call i32 @fibRec(i32 noundef %5), !dbg !128 + %7 = icmp eq i32 %2, %6, !dbg !129 + ret i1 %7, !dbg !123 +} + +; Function Attrs: noinline nounwind uwtable +define dso_local zeroext i1 @PALLAS_SPEC_5(i32 noundef %0, i32 noundef %1, i32 noundef %2, i32 noundef %3) #0 !dbg !130 !pallas.exprWrapper !95 { + call void @llvm.dbg.value(metadata i32 %0, metadata !131, metadata !DIExpression()), !dbg !132 + call void @llvm.dbg.value(metadata i32 %1, metadata !133, metadata !DIExpression()), !dbg !132 + call void @llvm.dbg.value(metadata i32 %2, metadata !134, metadata !DIExpression()), !dbg !132 + call void @llvm.dbg.value(metadata i32 %3, metadata !135, metadata !DIExpression()), !dbg !132 + %5 = sub nsw i32 %3, 2, !dbg !136 + %6 = call i32 @fibRec(i32 noundef %5), !dbg !137 + %7 = icmp eq i32 %1, %6, !dbg !138 + ret i1 %7, !dbg !132 +} + +declare !pallas.specLib !139 i32 @pallas.result.0() + +declare !pallas.specLib !140 i1 @pallas.scAnd(i1, i1) + +attributes #0 = { noinline nounwind uwtable "frame-pointer"="all" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cmov,+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" } +attributes #1 = { nocallback nofree nosync nounwind speculatable willreturn memory(none) } + +!llvm.dbg.cu = !{!0, !2} +!llvm.module.flags = !{!4, !5, !6, !7, !8, !9, !10} +!llvm.ident = !{!11, !11} + +!0 = distinct !DICompileUnit(language: DW_LANG_C11, file: !1, producer: "clang version 17.0.0 (https://github.com/swiftlang/llvm-project.git 73500bf55acff5fa97b56dcdeb013f288efd084f)", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, splitDebugInlining: false, nameTableKind: None) +!1 = !DIFile(filename: "examples/concepts/llvm/pallas/pallas_c_fibonacci.c", directory: ".", checksumkind: CSK_MD5, checksum: "66d6beef95c73c9cc2e6bdfa196e7ed3") +!2 = distinct !DICompileUnit(language: DW_LANG_C11, file: !3, producer: "clang version 17.0.0 (https://github.com/swiftlang/llvm-project.git 73500bf55acff5fa97b56dcdeb013f288efd084f)", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, splitDebugInlining: false, nameTableKind: None) +!3 = !DIFile(filename: "tmp/source_wrappers.c", directory: ".", checksumkind: CSK_MD5, checksum: "aa619c5f4f705d14d88bd20925b86f7f") +!4 = !{i32 7, !"Dwarf Version", i32 5} +!5 = !{i32 2, !"Debug Info Version", i32 3} +!6 = !{i32 1, !"wchar_size", i32 4} +!7 = !{i32 8, !"PIC Level", i32 2} +!8 = !{i32 7, !"PIE Level", i32 2} +!9 = !{i32 7, !"uwtable", i32 2} +!10 = !{i32 7, !"frame-pointer", i32 2} +!11 = !{!"clang version 17.0.0 (https://github.com/swiftlang/llvm-project.git 73500bf55acff5fa97b56dcdeb013f288efd084f)"} +!12 = distinct !DISubprogram(name: "fibRec", scope: !1, file: !1, line: 16, type: !13, scopeLine: 16, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !0, retainedNodes: !16) +!13 = !DISubroutineType(types: !14) +!14 = !{!15, !15} +!15 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed) +!16 = !{} +!17 = !{!18, i1 true, !19} +!18 = !{!"pallas.srcLoc", i64 12, i64 1, i64 15, i64 1} +!19 = !{!"pallas.requires", !20, ptr @PALLAS_SPEC_0, !21} +!20 = !{!"pallas.srcLoc", i64 14, i64 1, i64 14, i64 16} +!21 = !DILocalVariable(name: "n", arg: 1, scope: !12, file: !1, line: 16, type: !15) +!22 = !DILocation(line: 0, scope: !12) +!23 = !DILocation(line: 17, column: 11, scope: !24) +!24 = distinct !DILexicalBlock(scope: !12, file: !1, line: 17, column: 9) +!25 = !DILocation(line: 17, column: 9, scope: !12) +!26 = !DILocation(line: 18, column: 9, scope: !27) +!27 = distinct !DILexicalBlock(scope: !24, file: !1, line: 17, column: 17) +!28 = !DILocation(line: 19, column: 18, scope: !29) +!29 = distinct !DILexicalBlock(scope: !24, file: !1, line: 19, column: 16) +!30 = !DILocation(line: 19, column: 16, scope: !24) +!31 = !DILocation(line: 20, column: 9, scope: !32) +!32 = distinct !DILexicalBlock(scope: !29, file: !1, line: 19, column: 24) +!33 = !DILocation(line: 22, column: 25, scope: !34) +!34 = distinct !DILexicalBlock(scope: !29, file: !1, line: 21, column: 12) +!35 = !DILocation(line: 22, column: 16, scope: !34) +!36 = !DILocation(line: 22, column: 41, scope: !34) +!37 = !DILocation(line: 22, column: 32, scope: !34) +!38 = !DILocation(line: 22, column: 30, scope: !34) +!39 = !DILocation(line: 22, column: 9, scope: !34) +!40 = !DILocation(line: 0, scope: !24) +!41 = !DILocation(line: 24, column: 1, scope: !12) +!42 = distinct !DISubprogram(name: "fibIt", scope: !1, file: !1, line: 31, type: !13, scopeLine: 31, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !0, retainedNodes: !16) +!43 = !{!44, i1 false, !45, !48} +!44 = !{!"pallas.srcLoc", i64 27, i64 1, i64 30, i64 1} +!45 = !{!"pallas.requires", !46, ptr @PALLAS_SPEC_1, !47} +!46 = !{!"pallas.srcLoc", i64 28, i64 1, i64 28, i64 16} +!47 = !DILocalVariable(name: "n", arg: 1, scope: !42, file: !1, line: 31, type: !15) +!48 = !{!"pallas.ensures", !49, ptr @PALLAS_SPEC_2, !47} +!49 = !{!"pallas.srcLoc", i64 29, i64 1, i64 29, i64 35} +!50 = !DILocation(line: 0, scope: !42) +!51 = !DILocation(line: 32, column: 12, scope: !52) +!52 = distinct !DILexicalBlock(scope: !42, file: !1, line: 32, column: 10) +!53 = !DILocation(line: 32, column: 10, scope: !42) +!54 = !DILocation(line: 33, column: 9, scope: !55) +!55 = distinct !DILexicalBlock(scope: !52, file: !1, line: 32, column: 18) +!56 = !DILocation(line: 34, column: 20, scope: !57) +!57 = distinct !DILexicalBlock(scope: !52, file: !1, line: 34, column: 18) +!58 = !DILocation(line: 34, column: 18, scope: !52) +!59 = !DILocation(line: 35, column: 9, scope: !60) +!60 = distinct !DILexicalBlock(scope: !57, file: !1, line: 34, column: 26) +!61 = !DILocalVariable(name: "prevRes", scope: !42, file: !1, line: 38, type: !15) +!62 = !DILocalVariable(name: "res", scope: !42, file: !1, line: 39, type: !15) +!63 = !DILocalVariable(name: "i", scope: !64, file: !1, line: 46, type: !15) +!64 = distinct !DILexicalBlock(scope: !42, file: !1, line: 46, column: 5) +!65 = !DILocation(line: 0, scope: !64) +!66 = !DILocation(line: 46, column: 10, scope: !64) +!67 = !DILocation(line: 46, scope: !64) +!68 = !DILocation(line: 46, column: 23, scope: !69) +!69 = distinct !DILexicalBlock(scope: !64, file: !1, line: 46, column: 5) +!70 = !DILocation(line: 46, column: 5, scope: !64) +!71 = !DILocation(line: 47, column: 27, scope: !72) +!72 = distinct !DILexicalBlock(scope: !69, file: !1, line: 46, column: 34) +!73 = !DILocalVariable(name: "tmp", scope: !72, file: !1, line: 47, type: !15) +!74 = !DILocation(line: 0, scope: !72) +!75 = !DILocation(line: 50, column: 5, scope: !72) +!76 = !DILocation(line: 46, column: 30, scope: !69) +!77 = !DILocation(line: 46, column: 5, scope: !69) +!78 = distinct !{!78, !70, !79, !80, !81} +!79 = !DILocation(line: 50, column: 5, scope: !64) +!80 = !{!"llvm.loop.mustprogress"} +!81 = !{!"pallas.loopInv", !82, !83, !85, !87} +!82 = !{!"pallas.srcLoc", i64 41, i64 5, i64 45, i64 5} +!83 = !{!84, ptr @PALLAS_SPEC_3, !47, !61, !62, !63} +!84 = !{!"pallas.srcLoc", i64 42, i64 5, i64 42, i64 42} +!85 = !{!86, ptr @PALLAS_SPEC_4, !47, !61, !62, !63} +!86 = !{!"pallas.srcLoc", i64 43, i64 5, i64 43, i64 38} +!87 = !{!88, ptr @PALLAS_SPEC_5, !47, !61, !62, !63} +!88 = !{!"pallas.srcLoc", i64 44, i64 5, i64 44, i64 42} +!89 = !DILocation(line: 51, column: 5, scope: !42) +!90 = !DILocation(line: 52, column: 1, scope: !42) +!91 = distinct !DISubprogram(name: "PALLAS_SPEC_2", scope: !1, file: !1, line: 29, type: !92, scopeLine: 29, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !0, retainedNodes: !16) +!92 = !DISubroutineType(types: !93) +!93 = !{!94, !15} +!94 = !DIBasicType(name: "_Bool", size: 8, encoding: DW_ATE_boolean) +!95 = !{!""} +!96 = !DILocalVariable(name: "n", arg: 1, scope: !91, file: !1, line: 29, type: !15) +!97 = !DILocation(line: 0, scope: !91) +!98 = !DILocation(line: 29, column: 9, scope: !91) +!99 = !DILocation(line: 29, column: 26, scope: !91) +!100 = !DILocation(line: 29, column: 23, scope: !91) +!101 = distinct !DISubprogram(name: "PALLAS_SPEC_0", scope: !1, file: !1, line: 14, type: !92, scopeLine: 14, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !0, retainedNodes: !16) +!102 = !DILocalVariable(name: "n", arg: 1, scope: !101, file: !1, line: 14, type: !15) +!103 = !DILocation(line: 0, scope: !101) +!104 = !DILocation(line: 14, column: 12, scope: !101) +!105 = distinct !DISubprogram(name: "PALLAS_SPEC_1", scope: !1, file: !1, line: 28, type: !92, scopeLine: 28, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !0, retainedNodes: !16) +!106 = !DILocalVariable(name: "n", arg: 1, scope: !105, file: !1, line: 28, type: !15) +!107 = !DILocation(line: 0, scope: !105) +!108 = !DILocation(line: 28, column: 12, scope: !105) +!109 = distinct !DISubprogram(name: "PALLAS_SPEC_3", scope: !1, file: !1, line: 42, type: !110, scopeLine: 42, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !0, retainedNodes: !16) +!110 = !DISubroutineType(types: !111) +!111 = !{!94, !15, !15, !15, !15} +!112 = !DILocalVariable(name: "n", arg: 1, scope: !109, file: !1, line: 42, type: !15) +!113 = !DILocation(line: 0, scope: !109) +!114 = !DILocalVariable(name: "prevRes", arg: 2, scope: !109, file: !1, line: 42, type: !15) +!115 = !DILocalVariable(name: "res", arg: 3, scope: !109, file: !1, line: 42, type: !15) +!116 = !DILocalVariable(name: "i", arg: 4, scope: !109, file: !1, line: 42, type: !15) +!117 = !DILocation(line: 42, column: 27, scope: !109) +!118 = !DILocation(line: 42, column: 39, scope: !109) +!119 = !DILocation(line: 42, column: 35, scope: !109) +!120 = !DILocation(line: 42, column: 20, scope: !109) +!121 = distinct !DISubprogram(name: "PALLAS_SPEC_4", scope: !1, file: !1, line: 43, type: !110, scopeLine: 43, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !0, retainedNodes: !16) +!122 = !DILocalVariable(name: "n", arg: 1, scope: !121, file: !1, line: 43, type: !15) +!123 = !DILocation(line: 0, scope: !121) +!124 = !DILocalVariable(name: "prevRes", arg: 2, scope: !121, file: !1, line: 43, type: !15) +!125 = !DILocalVariable(name: "res", arg: 3, scope: !121, file: !1, line: 43, type: !15) +!126 = !DILocalVariable(name: "i", arg: 4, scope: !121, file: !1, line: 43, type: !15) +!127 = !DILocation(line: 43, column: 35, scope: !121) +!128 = !DILocation(line: 43, column: 27, scope: !121) +!129 = !DILocation(line: 43, column: 24, scope: !121) +!130 = distinct !DISubprogram(name: "PALLAS_SPEC_5", scope: !1, file: !1, line: 44, type: !110, scopeLine: 44, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !0, retainedNodes: !16) +!131 = !DILocalVariable(name: "n", arg: 1, scope: !130, file: !1, line: 44, type: !15) +!132 = !DILocation(line: 0, scope: !130) +!133 = !DILocalVariable(name: "prevRes", arg: 2, scope: !130, file: !1, line: 44, type: !15) +!134 = !DILocalVariable(name: "res", arg: 3, scope: !130, file: !1, line: 44, type: !15) +!135 = !DILocalVariable(name: "i", arg: 4, scope: !130, file: !1, line: 44, type: !15) +!136 = !DILocation(line: 44, column: 39, scope: !130) +!137 = !DILocation(line: 44, column: 31, scope: !130) +!138 = !DILocation(line: 44, column: 28, scope: !130) +!139 = !{!"pallas.result"} +!140 = !{!"pallas.scAnd"} diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index 6f9e3ca74..12e556329 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/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] diff --git a/src/col/vct/col/ast/lang/llvm/LLVMBasicBlockImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMBasicBlockImpl.scala index f9f0a1466..a82816d7c 100644 --- a/src/col/vct/col/ast/lang/llvm/LLVMBasicBlockImpl.scala +++ b/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("") <> Line <> loop.get.contract.show <> Line <> - label.show <> ":" <+> body.layoutAsBlock - } else { label.show <> ":" <+> body.layoutAsBlock } + Text("") <> Line <> loop.get.contract.show <> Line <> bodyDoc + } else { bodyDoc } } } diff --git a/src/llvm/include/Passes/Function/FunctionBodyTransformer.h b/src/llvm/include/Passes/Function/FunctionBodyTransformer.h index 1f166f245..e2cab7764 100644 --- a/src/llvm/include/Passes/Function/FunctionBodyTransformer.h +++ b/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 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 - 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 completedColBlocks; + /// All LLVM blocks mapped 1-to-1 to a COL block. + std::unordered_map + llvmBlock2ColBlock; /// set of all COL blocks that we have started transforming. - std::set visitedColBlocks; - - /// map of assignments which should be added to the basic block when it is - /// completed. - std::unordered_multimap 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, col::Block *> - phiAssignmentTargetMap; + std::set 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"
  • If a mapping between * the given LLVM block and a COL block already exists, return the COL * block
  • 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
    • *
* * @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 diff --git a/src/llvm/include/Passes/Function/PallasFunctionContractDeclarerPass.h b/src/llvm/include/Passes/Function/PallasFunctionContractDeclarerPass.h index 057c83f81..9047de76d 100644 --- a/src/llvm/include/Passes/Function/PallasFunctionContractDeclarerPass.h +++ b/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 diff --git a/src/llvm/include/Transform/BlockTransform.h b/src/llvm/include/Transform/BlockTransform.h index 2fe76a66b..1054fcce7 100644 --- a/src/llvm/include/Transform/BlockTransform.h +++ b/src/llvm/include/Transform/BlockTransform.h @@ -11,7 +11,7 @@ namespace col = vct::col::ast; *
  • Create or fetch the corresponding labeled col block from the function * cursor
  • Check if all predecessor blocks have been visited yet, * otherwise, return
  • If block turns out to be a loop header, hand over - * transformation of the loo-contract to LoopContractTransform. + * transformation of the loo-contract to LoopContractTransform. *
    • *
  • Transform instructions of the block
    • * @@ -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); diff --git a/src/llvm/include/Transform/Instruction/BinaryOpTransform.h b/src/llvm/include/Transform/Instruction/BinaryOpTransform.h index 8e965b2bf..e9ee68874 100644 --- a/src/llvm/include/Transform/Instruction/BinaryOpTransform.h +++ b/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 diff --git a/src/llvm/include/Transform/Instruction/CastOpTransform.h b/src/llvm/include/Transform/Instruction/CastOpTransform.h index d731fd8cb..b5bf152c0 100644 --- a/src/llvm/include/Transform/Instruction/CastOpTransform.h +++ b/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 diff --git a/src/llvm/include/Transform/Instruction/FuncletPadOpTransform.h b/src/llvm/include/Transform/Instruction/FuncletPadOpTransform.h index ae810415b..086370cc1 100644 --- a/src/llvm/include/Transform/Instruction/FuncletPadOpTransform.h +++ b/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 diff --git a/src/llvm/include/Transform/Instruction/MemoryOpTransform.h b/src/llvm/include/Transform/Instruction/MemoryOpTransform.h index 71707639f..5c853f4d8 100644 --- a/src/llvm/include/Transform/Instruction/MemoryOpTransform.h +++ b/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 diff --git a/src/llvm/include/Transform/Instruction/OtherOpTransform.h b/src/llvm/include/Transform/Instruction/OtherOpTransform.h index d6fdd27e3..a04d06bbe 100644 --- a/src/llvm/include/Transform/Instruction/OtherOpTransform.h +++ b/src/llvm/include/Transform/Instruction/OtherOpTransform.h @@ -5,7 +5,8 @@ namespace llvm2col { namespace col = vct::col::ast; -void transformOtherOp(llvm::Instruction &llvmInstruction, col::Block &colBlock, +void transformOtherOp(llvm::Instruction &llvmInstruction, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); /** * Phi nodes get transformed retroactively by creating a variable declaration @@ -15,10 +16,11 @@ void transformOtherOp(llvm::Instruction &llvmInstruction, col::Block &colBlock, * @param colBlock Col-block of the phi instruction * @param funcCursor */ -void transformPhi(llvm::PHINode &phiInstruction, col::Block &colBlock, +void transformPhi(llvm::PHINode &phiInstruction, col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); -void transformICmp(llvm::ICmpInst &icmpInstruction, col::Block &colBlock, +void transformICmp(llvm::ICmpInst &icmpInstruction, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); /** * Transforms the common part of all compare instructions (the argument pair). @@ -31,10 +33,12 @@ void transformICmp(llvm::ICmpInst &icmpInstruction, col::Block &colBlock, void transformCmpExpr(llvm::CmpInst &cmpInstruction, auto &colCompareExpr, pallas::FunctionCursor &funcCursor); -void transformCallExpr(llvm::CallInst &callInstruction, col::Block &colBlock, +void transformCallExpr(llvm::CallInst &callInstruction, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); -void transformFCmp(llvm::FCmpInst &fcmpInstruction, col::Block &colBlock, +void transformFCmp(llvm::FCmpInst &fcmpInstruction, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); bool checkCallSupport(llvm::CallInst &callInstruction); @@ -44,7 +48,7 @@ bool checkCallSupport(llvm::CallInst &callInstruction); * appropriate specification construct. */ void transformPallasSpecLibCall(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); /** @@ -54,7 +58,7 @@ void transformPallasSpecLibCall(llvm::CallInst &callInstruction, * of the pallas specification library. */ void transformPallasSpecResult(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); /** @@ -62,57 +66,63 @@ void transformPallasSpecResult(llvm::CallInst &callInstruction, * specification library. */ void transformPallasFracOf(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); /** * Transform call-instruction to the Perm-function of the pallas * specification library. */ -void transformPallasPerm(llvm::CallInst &callInstruction, col::Block &colBlock, +void transformPallasPerm(llvm::CallInst &callInstruction, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); void transformPallasPtrBlockLength(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); void transformPallasPtrBlockOffset(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); void transformPallasPtrLength(llvm::CallInst &callInstruction, - col::Block &colBlock, - pallas::FunctionCursor &funcCursor); + col::LlvmBasicBlock &colBlock, + pallas::FunctionCursor &funcCursor); -void transformPallasImply(llvm::CallInst &callInstruction, col::Block &colBlock, +void transformPallasImply(llvm::CallInst &callInstruction, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); -void transformPallasAnd(llvm::CallInst &callInstruction, col::Block &colBlock, +void transformPallasAnd(llvm::CallInst &callInstruction, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); -void transformPallasOr(llvm::CallInst &callInstruction, col::Block &colBlock, +void transformPallasOr(llvm::CallInst &callInstruction, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); -void transformPallasStar(llvm::CallInst &callInstruction, col::Block &colBlock, +void transformPallasStar(llvm::CallInst &callInstruction, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); -void transformPallasOld(llvm::CallInst &callInstruction, col::Block &colBlock, +void transformPallasOld(llvm::CallInst &callInstruction, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); void transformPallasBoundVar(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); void transformPallasForall(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); void transformPallasSepForall(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); void transformPallasExists(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); } // namespace llvm2col diff --git a/src/llvm/include/Transform/Instruction/TermOpTransform.h b/src/llvm/include/Transform/Instruction/TermOpTransform.h index 3f50a9501..5a1c59f9c 100644 --- a/src/llvm/include/Transform/Instruction/TermOpTransform.h +++ b/src/llvm/include/Transform/Instruction/TermOpTransform.h @@ -6,21 +6,23 @@ namespace llvm2col { namespace col = vct::col::ast; -void transformTermOp(llvm::Instruction &llvmInstruction, col::Block &colBlock, +void transformTermOp(llvm::Instruction &llvmInstruction, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); -void transformRet(llvm::ReturnInst &llvmRetInstruction, col::Block &colBlock, +void transformRet(llvm::ReturnInst &llvmRetInstruction, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); void transformConditionalBranch(llvm::BranchInst &llvmBrInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); void transformUnConditionalBranch(llvm::BranchInst &llvmBrInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); void transformUnreachable(llvm::UnreachableInst &llvmUnreachableInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); } // namespace llvm2col #endif // PALLAS_TERMOPTRANSFORM_H diff --git a/src/llvm/include/Transform/Instruction/UnaryOpTransform.h b/src/llvm/include/Transform/Instruction/UnaryOpTransform.h index 2995eb075..3edd0204d 100644 --- a/src/llvm/include/Transform/Instruction/UnaryOpTransform.h +++ b/src/llvm/include/Transform/Instruction/UnaryOpTransform.h @@ -6,7 +6,8 @@ namespace llvm2col { namespace col = vct::col::ast; -void transformUnaryOp(llvm::Instruction &llvmInstruction, col::Block &colBlock, +void transformUnaryOp(llvm::Instruction &llvmInstruction, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor); } // namespace llvm2col #endif // PALLAS_UNARYOPTRANSFORM_H diff --git a/src/llvm/include/Util/BlockUtils.h b/src/llvm/include/Util/BlockUtils.h new file mode 100644 index 000000000..ab640ea98 --- /dev/null +++ b/src/llvm/include/Util/BlockUtils.h @@ -0,0 +1,12 @@ +#ifndef PALLAS_BLOCKUTILS_H +#define PALLAS_BLOCKUTILS_H + +#include "vct/col/ast/col.pb.h" + +namespace pallas { +namespace col = vct::col::ast; + +col::Block &bodyAsBlock(col::LlvmBasicBlock &llvmBB); + +} // namespace pallas +#endif // PALLAS_BLOCKUTILS_H diff --git a/src/llvm/include/Util/Constants.h b/src/llvm/include/Util/Constants.h index 742f72004..409812e73 100644 --- a/src/llvm/include/Util/Constants.h +++ b/src/llvm/include/Util/Constants.h @@ -31,7 +31,6 @@ const std::string PALLAS_SPEC_FORALL = "pallas.forall"; const std::string PALLAS_SPEC_SEPFORALL = "pallas.forallSep"; const std::string PALLAS_SPEC_EXISTS = "pallas.exists"; - // Legacy VCLLVM constants const std::string VC_PREFIX = "VC."; diff --git a/src/llvm/include/Util/PallasMD.h b/src/llvm/include/Util/PallasMD.h index a97cb3365..0fe658b28 100644 --- a/src/llvm/include/Util/PallasMD.h +++ b/src/llvm/include/Util/PallasMD.h @@ -56,8 +56,8 @@ bool isWellformedPallasLocation(const llvm::MDNode *mdNode); llvm::MDNode *getPallasLoopContract(const llvm::Loop &llvmLoop); /* - * Attempts to get the wrapper-function from the given MDNode which - * represents a Pallas loop-invariant clause. + * Attempts to get the wrapper-function from the given MDNode which + * represents a Pallas loop-invariant clause. * Returns nullptr on failure. */ llvm::Function *getWrapperFromLoopInv(const llvm::MDNode &invMD); diff --git a/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp b/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp index e1d72183d..d58489e42 100644 --- a/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp +++ b/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp @@ -5,6 +5,7 @@ #include "Passes/Function/FunctionDeclarer.h" #include "Transform/BlockTransform.h" #include "Transform/Transform.h" +#include "Util/BlockUtils.h" #include "Util/Exceptions.h" #include @@ -60,31 +61,12 @@ col::Variable &FunctionCursor::getVariableMapEntry(Value &llvmValue, bool FunctionCursor::isVisited(BasicBlock &llvmBlock) { return visitedColBlocks.contains( - &this->getOrSetLLVMBlock2LabeledColBlockEntry(llvmBlock).block); + &this->getOrSetLLVMBlock2ColBlockEntry(llvmBlock)); } -void FunctionCursor::complete(col::Block &colBlock) { - int lastIndex = colBlock.statements_size() - 1; - bool found = false; - auto range = phiAssignBuffer.equal_range(&colBlock); - for (auto it = range.first; it != range.second; ++it) { - found = true; - colBlock.add_statements()->set_allocated_assign(it->second); - } - if (found) { - colBlock.mutable_statements()->SwapElements( - colBlock.statements_size() - 1, lastIndex); - } - completedColBlocks.insert(&colBlock); -} - -bool FunctionCursor::isComplete(col::Block &colBlock) { - return completedColBlocks.contains(&colBlock); -} - -LabeledColBlock & -FunctionCursor::getOrSetLLVMBlock2LabeledColBlockEntry(BasicBlock &llvmBlock) { - if (!llvmBlock2LabeledColBlock.contains(&llvmBlock)) { +col::LlvmBasicBlock & +FunctionCursor::getOrSetLLVMBlock2ColBlockEntry(BasicBlock &llvmBlock) { + if (!llvmBlock2ColBlock.contains(&llvmBlock)) { // create basic block in buffer col::LlvmBasicBlock *bb = functionBody.add_statements()->mutable_llvm_basic_block(); @@ -101,36 +83,15 @@ FunctionCursor::getOrSetLLVMBlock2LabeledColBlockEntry(BasicBlock &llvmBlock) { col::Block *block = bb->mutable_body()->mutable_block(); // set block origin block->set_allocated_origin(llvm2col::generateBlockOrigin(llvmBlock)); - // add labeled block to the block2block lut - LabeledColBlock labeledColBlock = {*bb, *block}; - llvmBlock2LabeledColBlock.insert({&llvmBlock, labeledColBlock}); + llvmBlock2ColBlock.insert({&llvmBlock, *bb}); } - return llvmBlock2LabeledColBlock.at(&llvmBlock); -} - -LabeledColBlock FunctionCursor::generateIntermediaryLabeledColBlock( - llvm::Instruction &originInstruction) { - // create basic block - col::LlvmBasicBlock *bb = - functionBody.add_statements()->mutable_llvm_basic_block(); - bb->set_allocated_origin( - llvm2col::generateSingleStatementOrigin(originInstruction)); - // create label declaration in buffer - col::LabelDecl *labelDecl = bb->mutable_label(); - labelDecl->set_allocated_origin( - llvm2col::generateSingleStatementOrigin(originInstruction)); - llvm2col::setColNodeId(labelDecl); - // create nested block - col::Block *block = bb->mutable_body()->mutable_block(); - block->set_allocated_origin( - llvm2col::generateSingleStatementOrigin(originInstruction)); - return {*bb, *block}; + return llvmBlock2ColBlock.at(&llvmBlock); } -LabeledColBlock &FunctionCursor::visitLLVMBlock(BasicBlock &llvmBlock) { - LabeledColBlock &labeledBlock = - this->getOrSetLLVMBlock2LabeledColBlockEntry(llvmBlock); - visitedColBlocks.insert(&labeledBlock.block); +col::LlvmBasicBlock &FunctionCursor::visitLLVMBlock(BasicBlock &llvmBlock) { + col::LlvmBasicBlock &labeledBlock = + this->getOrSetLLVMBlock2ColBlockEntry(llvmBlock); + visitedColBlocks.insert(&labeledBlock); return labeledBlock; } @@ -185,16 +146,19 @@ col::Variable &FunctionCursor::declareVariable(Instruction &llvmInstruction, return *varDecl; } -col::Assign &FunctionCursor::createAssignmentAndDeclaration( - Instruction &llvmInstruction, col::Block &colBlock, Type *llvmPointerType) { +col::Assign & +FunctionCursor::createAssignmentAndDeclaration(Instruction &llvmInstruction, + col::LlvmBasicBlock &colBlock, + Type *llvmPointerType) { col::Variable &varDecl = declareVariable(llvmInstruction, llvmPointerType); return createAssignment(llvmInstruction, colBlock, varDecl); } col::Assign &FunctionCursor::createAssignment(Instruction &llvmInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, col::Variable &varDecl) { - col::Assign *assignment = colBlock.add_statements()->mutable_assign(); + col::Block &body = pallas::bodyAsBlock(colBlock); + col::Assign *assignment = body.add_statements()->mutable_assign(); assignment->set_allocated_blame(new col::Blame()); assignment->set_allocated_origin( llvm2col::generateSingleStatementOrigin(llvmInstruction)); @@ -204,22 +168,14 @@ col::Assign &FunctionCursor::createAssignment(Instruction &llvmInstruction, llvm2col::generateAssignTargetOrigin(llvmInstruction)); // set target to refer to var decl colLocal->mutable_ref()->set_id(varDecl.id()); - if (isComplete(colBlock)) { - // if the colBlock is completed, the assignment will be inserted after - // the goto/branch statement this can occur due to e.g. phi nodes back - // tracking assignments in their origin blocks. therefore we need to - // swap the last two elements of the block (i.e. the goto statement and - // the newest assignment) - int lastIndex = colBlock.statements_size() - 1; - colBlock.mutable_statements()->SwapElements(lastIndex, lastIndex - 1); - } return *assignment; } col::Assign &FunctionCursor::createPhiAssignment(Instruction &llvmInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, col::Variable &varDecl) { - col::Assign *assignment = new col::Assign(); + // col::Assign *assignment = new col::Assign(); + col::Assign *assignment = colBlock.add_phi_assignments()->mutable_assign(); assignment->set_allocated_blame(new col::Blame()); assignment->set_allocated_origin( llvm2col::generateSingleStatementOrigin(llvmInstruction)); @@ -229,39 +185,9 @@ col::Assign &FunctionCursor::createPhiAssignment(Instruction &llvmInstruction, llvm2col::generateAssignTargetOrigin(llvmInstruction)); // set target to refer to var decl colLocal->mutable_ref()->set_id(varDecl.id()); - if (isComplete(colBlock)) { - // if the colBlock is completed, the assignment will be inserted after - // the goto/branch statement this can occur due to e.g. phi nodes back - // tracking assignments in their origin blocks. therefore we need to - // swap the last two elements of the block (i.e. the goto statement and - // the newest assignment) - colBlock.add_statements()->set_allocated_assign(assignment); - int lastIndex = colBlock.statements_size() - 1; - colBlock.mutable_statements()->SwapElements(lastIndex, lastIndex - 1); - } else { - // Buffer the phi assignments so they appear at the end - phiAssignBuffer.insert({&colBlock, assignment}); - } return *assignment; } -void FunctionCursor::addNewPhiAssignmentTargetBlock(col::Block &from, - col::Block &toPhi, - col::Block &newBlock) { - phiAssignmentTargetMap.insert({{&from, &toPhi}, &newBlock}); -} - -col::Block *FunctionCursor::getTargetForPhiAssignment(col::Block &from, - col::Block &to) { - auto res = phiAssignmentTargetMap.find({&from, &to}); - if (res == phiAssignmentTargetMap.end()) { - // If the map does not contain an entry, no intermediary block has been - // added. - return &from; - } - return res->second; -} - llvm::FunctionAnalysisManager &FunctionCursor::getFunctionAnalysisManager() { return FAM; } diff --git a/src/llvm/lib/Passes/Function/FunctionContractDeclarer.cpp b/src/llvm/lib/Passes/Function/FunctionContractDeclarer.cpp index 977feffa2..533659709 100644 --- a/src/llvm/lib/Passes/Function/FunctionContractDeclarer.cpp +++ b/src/llvm/lib/Passes/Function/FunctionContractDeclarer.cpp @@ -45,7 +45,8 @@ FunctionContractDeclarerPass::run(Function &F, FunctionAnalysisManager &FAM) { // get col contract FDCResult result = FAM.getResult(F); col::VcllvmFunctionContract *colContract = - result.getAssociatedColFuncContract().mutable_vcllvm_function_contract(); + result.getAssociatedColFuncContract() + .mutable_vcllvm_function_contract(); colContract->set_allocated_blame(new col::Blame()); colContract->set_name(F.getName()); // check if contract keyword is present diff --git a/src/llvm/lib/Plugin.cpp b/src/llvm/lib/Plugin.cpp index 0ec330bbc..01c6581e4 100644 --- a/src/llvm/lib/Plugin.cpp +++ b/src/llvm/lib/Plugin.cpp @@ -3,8 +3,8 @@ #include "Passes/Function/FunctionBodyTransformer.h" #include "Passes/Function/FunctionContractDeclarer.h" #include "Passes/Function/FunctionDeclarer.h" -#include "Passes/Function/PureAssigner.h" #include "Passes/Function/PallasFunctionContractDeclarerPass.h" +#include "Passes/Function/PureAssigner.h" #include "Passes/Module/GlobalVariableDeclarer.h" #include "Passes/Module/ModuleSpecCollector.h" #include "Passes/Module/ProtobufPrinter.h" @@ -60,12 +60,13 @@ llvm::PassPluginLibraryInfo getPallasPluginInfo() { FPM.addPass(pallas::FunctionContractDeclarerPass()); return true; } else if (Name == "pallas-declare-function-contract") { - FPM.addPass(pallas::PallasFunctionContractDeclarerPass()); + FPM.addPass( + pallas::PallasFunctionContractDeclarerPass()); return true; } else if (Name == "pallas-transform-function-body") { FPM.addPass(pallas::FunctionBodyTransformerPass()); return true; - } + } return false; }); }}; diff --git a/src/llvm/lib/Transform/BlockTransform.cpp b/src/llvm/lib/Transform/BlockTransform.cpp index d7cc50031..d85669999 100644 --- a/src/llvm/lib/Transform/BlockTransform.cpp +++ b/src/llvm/lib/Transform/BlockTransform.cpp @@ -18,45 +18,34 @@ void llvm2col::transformLLVMBlock(llvm::BasicBlock &llvmBlock, if (functionCursor.isVisited(llvmBlock)) { return; } - pallas::LabeledColBlock &labeled = functionCursor.visitLLVMBlock(llvmBlock); - col::Block &colBlock = labeled.block; - /* for (auto *B : llvm::predecessors(&llvmBlock)) { */ - /* if (!functionCursor.isVisited(*B)) */ - /* return; */ - /* } */ + col::LlvmBasicBlock &labeled = functionCursor.visitLLVMBlock(llvmBlock); if (functionCursor.getLoopInfo().isLoopHeader(&llvmBlock)) { llvm::Loop *llvmLoop = functionCursor.getLoopInfo().getLoopFor(&llvmBlock); - col::LlvmLoop *loop = labeled.bb.mutable_loop(); + col::LlvmLoop *loop = labeled.mutable_loop(); loop->set_allocated_origin(generateLoopOrigin(*llvmLoop)); transformLoopContract(*llvmLoop, *loop->mutable_contract(), functionCursor); - loop->mutable_header()->set_id(labeled.bb.label().id()); - pallas::LabeledColBlock labeled_latch = - functionCursor.getOrSetLLVMBlock2LabeledColBlockEntry( + loop->mutable_header()->set_id(labeled.label().id()); + col::LlvmBasicBlock &labeled_latch = + functionCursor.getOrSetLLVMBlock2ColBlockEntry( *llvmLoop->getLoopLatch()); - loop->mutable_latch()->set_id(labeled_latch.bb.label().id()); + loop->mutable_latch()->set_id(labeled_latch.label().id()); for (auto &bb : llvmLoop->blocks()) { - pallas::LabeledColBlock labeled_bb = - functionCursor.getOrSetLLVMBlock2LabeledColBlockEntry(*bb); - loop->add_block_labels()->set_id(labeled_bb.bb.label().id()); + col::LlvmBasicBlock &labeled_bb = + functionCursor.getOrSetLLVMBlock2ColBlockEntry(*bb); + loop->add_block_labels()->set_id(labeled_bb.label().id()); } } for (auto &I : llvmBlock) { - transformInstruction(functionCursor, I, colBlock); - } - - // When the last instuction is a branch, the block already gets completed - // in the call to transformInstruction. - if (!functionCursor.isComplete(colBlock)) { - functionCursor.complete(colBlock); + transformInstruction(functionCursor, I, labeled); } } void llvm2col::transformInstruction(pallas::FunctionCursor &funcCursor, llvm::Instruction &llvmInstruction, - col::Block &colBodyBlock) { + col::LlvmBasicBlock &colBodyBlock) { u_int32_t opCode = llvmInstruction.getOpcode(); if (llvm::Instruction::TermOpsBegin <= opCode && opCode < llvm::Instruction::TermOpsEnd) { diff --git a/src/llvm/lib/Transform/Instruction/BinaryOpTransform.cpp b/src/llvm/lib/Transform/Instruction/BinaryOpTransform.cpp index 48d056407..dbaa56af6 100644 --- a/src/llvm/lib/Transform/Instruction/BinaryOpTransform.cpp +++ b/src/llvm/lib/Transform/Instruction/BinaryOpTransform.cpp @@ -8,7 +8,7 @@ const std::string SOURCE_LOC = "Transform::Instruction::BinaryOp"; void llvm2col::transformBinaryOp(llvm::Instruction &llvmInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { col::Assign &assignment = funcCursor.createAssignmentAndDeclaration(llvmInstruction, colBlock); diff --git a/src/llvm/lib/Transform/Instruction/CastOpTransform.cpp b/src/llvm/lib/Transform/Instruction/CastOpTransform.cpp index 62e926025..b3f49c465 100644 --- a/src/llvm/lib/Transform/Instruction/CastOpTransform.cpp +++ b/src/llvm/lib/Transform/Instruction/CastOpTransform.cpp @@ -6,7 +6,7 @@ const std::string SOURCE_LOC = "Transform::Instruction::CastOp"; void llvm2col::transformCastOp(llvm::Instruction &llvmInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { switch (llvm::Instruction::CastOps(llvmInstruction.getOpcode())) { case llvm::Instruction::SExt: @@ -31,7 +31,7 @@ void llvm2col::transformCastOp(llvm::Instruction &llvmInstruction, } void llvm2col::transformSExt(llvm::SExtInst &sextInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { col::Assign &assignment = funcCursor.createAssignmentAndDeclaration(sextInstruction, colBlock); @@ -49,7 +49,7 @@ void llvm2col::transformSExt(llvm::SExtInst &sextInstruction, } void llvm2col::transformZExt(llvm::ZExtInst &zextInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { col::Assign &assignment = funcCursor.createAssignmentAndDeclaration(zextInstruction, colBlock); @@ -67,7 +67,7 @@ void llvm2col::transformZExt(llvm::ZExtInst &zextInstruction, } void llvm2col::transformTrunc(llvm::TruncInst &truncInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { col::Assign &assignment = funcCursor.createAssignmentAndDeclaration(truncInstruction, colBlock); @@ -85,7 +85,7 @@ void llvm2col::transformTrunc(llvm::TruncInst &truncInstruction, } void llvm2col::transformFPExt(llvm::FPExtInst &fpextInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { col::Assign &assignment = funcCursor.createAssignmentAndDeclaration(fpextInstruction, colBlock); diff --git a/src/llvm/lib/Transform/Instruction/FuncletPadOpTransform.cpp b/src/llvm/lib/Transform/Instruction/FuncletPadOpTransform.cpp index 104b71d3c..8d2cddc58 100644 --- a/src/llvm/lib/Transform/Instruction/FuncletPadOpTransform.cpp +++ b/src/llvm/lib/Transform/Instruction/FuncletPadOpTransform.cpp @@ -6,7 +6,7 @@ const std::string SOURCE_LOC = "Transform::Instruction::FuncletPadOp"; void llvm2col::transformFuncletPadOp(llvm::Instruction &llvmInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { // TODO stub reportUnsupportedOperatorError(SOURCE_LOC, llvmInstruction); diff --git a/src/llvm/lib/Transform/Instruction/MemoryOpTransform.cpp b/src/llvm/lib/Transform/Instruction/MemoryOpTransform.cpp index 864245eab..93df667e3 100644 --- a/src/llvm/lib/Transform/Instruction/MemoryOpTransform.cpp +++ b/src/llvm/lib/Transform/Instruction/MemoryOpTransform.cpp @@ -3,13 +3,14 @@ #include "Origin/OriginProvider.h" #include "Transform/BlockTransform.h" #include "Transform/Transform.h" +#include "Util/BlockUtils.h" #include "Util/Exceptions.h" #include const std::string SOURCE_LOC = "Transform::Instruction::MemoryOp"; void llvm2col::transformMemoryOp(llvm::Instruction &llvmInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { switch (llvm::Instruction::MemoryOps(llvmInstruction.getOpcode())) { case llvm::Instruction::Alloca: @@ -35,9 +36,10 @@ void llvm2col::transformMemoryOp(llvm::Instruction &llvmInstruction, } void llvm2col::transformAllocA(llvm::AllocaInst &allocAInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { - col::LlvmAllocA *allocA = colBlock.add_statements()->mutable_llvm_alloc_a(); + col::LlvmAllocA *allocA = + pallas::bodyAsBlock(colBlock).add_statements()->mutable_llvm_alloc_a(); allocA->set_allocated_origin( llvm2col::generateSingleStatementOrigin(allocAInstruction)); @@ -106,10 +108,11 @@ void llvm2col::transformAtomicOrdering(llvm::AtomicOrdering ordering, } void llvm2col::transformLoad(llvm::LoadInst &loadInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { // We are not storing isVolatile and getAlign - col::LlvmLoad *load = colBlock.add_statements()->mutable_llvm_load(); + col::LlvmLoad *load = + pallas::bodyAsBlock(colBlock).add_statements()->mutable_llvm_load(); load->set_allocated_origin( llvm2col::generateSingleStatementOrigin(loadInstruction)); load->set_allocated_blame(new col::Blame()); @@ -125,10 +128,11 @@ void llvm2col::transformLoad(llvm::LoadInst &loadInstruction, } void llvm2col::transformStore(llvm::StoreInst &storeInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { // We are not storing isVolatile and getAlign - col::LlvmStore *store = colBlock.add_statements()->mutable_llvm_store(); + col::LlvmStore *store = + pallas::bodyAsBlock(colBlock).add_statements()->mutable_llvm_store(); store->set_allocated_origin( llvm2col::generateSingleStatementOrigin(storeInstruction)); store->set_allocated_blame(new col::Blame()); @@ -143,7 +147,7 @@ void llvm2col::transformStore(llvm::StoreInst &storeInstruction, } void llvm2col::transformGetElementPtr(llvm::GetElementPtrInst &gepInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { col::Assign &assignment = funcCursor.createAssignmentAndDeclaration( diff --git a/src/llvm/lib/Transform/Instruction/OtherOpTransform.cpp b/src/llvm/lib/Transform/Instruction/OtherOpTransform.cpp index 4ea50df7a..ebb059be7 100644 --- a/src/llvm/lib/Transform/Instruction/OtherOpTransform.cpp +++ b/src/llvm/lib/Transform/Instruction/OtherOpTransform.cpp @@ -11,6 +11,7 @@ #include "Passes/Function/ExprWrapperMapper.h" #include "Transform/BlockTransform.h" #include "Transform/Transform.h" +#include "Util/BlockUtils.h" #include "Util/Constants.h" #include "Util/Exceptions.h" #include "Util/PallasMD.h" @@ -18,7 +19,7 @@ const std::string SOURCE_LOC = "Transform::Instruction::OtherOp"; void llvm2col::transformOtherOp(llvm::Instruction &llvmInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { switch (llvm::Instruction::OtherOps(llvmInstruction.getOpcode())) { case llvm::Instruction::PHI: @@ -42,21 +43,18 @@ void llvm2col::transformOtherOp(llvm::Instruction &llvmInstruction, } } -void llvm2col::transformPhi(llvm::PHINode &phiInstruction, col::Block &colBlock, +void llvm2col::transformPhi(llvm::PHINode &phiInstruction, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { col::Variable &varDecl = funcCursor.declareVariable(phiInstruction); for (auto &B : phiInstruction.blocks()) { // add assignment of the variable to the block of the conditional // branch - col::Block &targetBlock = - funcCursor.getOrSetLLVMBlock2LabeledColBlockEntry(*B).block; - // In some cases, the phi-assignments needs to be re-targeted to an - // empty block. - col::Block *newTargetBlock = - funcCursor.getTargetForPhiAssignment(targetBlock, colBlock); + col::LlvmBasicBlock &targetBlock = + funcCursor.getOrSetLLVMBlock2ColBlockEntry(*B); col::Assign &assignment = funcCursor.createPhiAssignment( - phiInstruction, *newTargetBlock, varDecl); + phiInstruction, targetBlock, varDecl); // assign correct value by looking at the value-block pair of phi // instruction. col::Expr *value = assignment.mutable_value(); @@ -67,7 +65,7 @@ void llvm2col::transformPhi(llvm::PHINode &phiInstruction, col::Block &colBlock, } void llvm2col::transformICmp(llvm::ICmpInst &icmpInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { col::Assign &assignment = funcCursor.createAssignmentAndDeclaration(icmpInstruction, colBlock); @@ -113,7 +111,7 @@ void llvm2col::transformICmp(llvm::ICmpInst &icmpInstruction, } void llvm2col::transformFCmp(llvm::FCmpInst &fcmpInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { // TODO: Deal with fastmath flags // TODO: Deal with NaNs, LLVM generally pretends signalling NaNs don't @@ -250,7 +248,7 @@ bool llvm2col::checkCallSupport(llvm::CallInst &callInstruction) { } void llvm2col::transformCallExpr(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { if (!checkCallSupport(callInstruction) || callInstruction.getCalledFunction() == nullptr) @@ -272,7 +270,8 @@ void llvm2col::transformCallExpr(llvm::CallInst &callInstruction, col::Expr *functionCallExpr; // if void function add an eval expression if (callInstruction.getType()->isVoidTy()) { - col::Eval *eval = colBlock.add_statements()->mutable_eval(); + col::Eval *eval = + pallas::bodyAsBlock(colBlock).add_statements()->mutable_eval(); eval->set_allocated_origin( llvm2col::generateSingleStatementOrigin(callInstruction)); functionCallExpr = eval->mutable_expr(); @@ -300,7 +299,7 @@ void llvm2col::transformCallExpr(llvm::CallInst &callInstruction, } void llvm2col::transformPallasSpecLibCall(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { auto specLibType = pallas::utils::isPallasSpecLib(*callInstruction.getCalledFunction()) @@ -392,7 +391,7 @@ bool checkPtrBlockSpecFuncWellformed(llvm::Function &specFunc, } // namespace void llvm2col::transformPallasSpecResult(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { auto *llvmSpecFunc = callInstruction.getCalledFunction(); bool isRegularReturn = !llvmSpecFunc->getReturnType()->isVoidTy(); @@ -451,7 +450,9 @@ void llvm2col::transformPallasSpecResult(llvm::CallInst &callInstruction, // Replace the call to the result-function with a store-instruction that // stores the value of \result. - col::LlvmStore *store = colBlock.add_statements()->mutable_llvm_store(); + col::LlvmStore *store = pallas::bodyAsBlock(colBlock) + .add_statements() + ->mutable_llvm_store(); store->set_allocated_origin( llvm2col::generateFunctionCallOrigin(callInstruction)); store->set_allocated_blame(new col::Blame()); @@ -474,7 +475,7 @@ void llvm2col::transformPallasSpecResult(llvm::CallInst &callInstruction, } void llvm2col::transformPallasFracOf(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { auto *llvmSpecFunc = callInstruction.getCalledFunction(); @@ -500,7 +501,8 @@ void llvm2col::transformPallasFracOf(llvm::CallInst &callInstruction, return; } - col::LlvmFracOf *fracOf = colBlock.add_statements()->mutable_llvm_frac_of(); + col::LlvmFracOf *fracOf = + pallas::bodyAsBlock(colBlock).add_statements()->mutable_llvm_frac_of(); fracOf->set_allocated_origin( llvm2col::generateFunctionCallOrigin(callInstruction)); fracOf->set_allocated_blame(new col::Blame()); @@ -516,7 +518,7 @@ void llvm2col::transformPallasFracOf(llvm::CallInst &callInstruction, } void llvm2col::transformPallasPerm(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { // Check that the function signature is wellformed auto *llvmSpecFunc = callInstruction.getCalledFunction(); @@ -545,7 +547,7 @@ void llvm2col::transformPallasPerm(llvm::CallInst &callInstruction, } void llvm2col::transformPallasPtrBlockLength( - llvm::CallInst &callInstruction, col::Block &colBlock, + llvm::CallInst &callInstruction, col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { auto *llvmSpecFunc = callInstruction.getCalledFunction(); if (!checkPtrBlockSpecFuncWellformed(*llvmSpecFunc, "PtrBlockLength")) { @@ -564,7 +566,7 @@ void llvm2col::transformPallasPtrBlockLength( } void llvm2col::transformPallasPtrBlockOffset( - llvm::CallInst &callInstruction, col::Block &colBlock, + llvm::CallInst &callInstruction, col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { auto *llvmSpecFunc = callInstruction.getCalledFunction(); if (!checkPtrBlockSpecFuncWellformed(*llvmSpecFunc, "PtrBlockOffset")) { @@ -583,7 +585,7 @@ void llvm2col::transformPallasPtrBlockOffset( } void llvm2col::transformPallasPtrLength(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { auto *llvmSpecFunc = callInstruction.getCalledFunction(); if (!checkPtrBlockSpecFuncWellformed(*llvmSpecFunc, "PtrLength")) { @@ -602,7 +604,7 @@ void llvm2col::transformPallasPtrLength(llvm::CallInst &callInstruction, } void llvm2col::transformPallasImply(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { auto *llvmSpecFunc = callInstruction.getCalledFunction(); // Check that the function signature is wellformed @@ -624,7 +626,7 @@ void llvm2col::transformPallasImply(llvm::CallInst &callInstruction, } void llvm2col::transformPallasAnd(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { auto *llvmSpecFunc = callInstruction.getCalledFunction(); // Check that the function signature is wellformed @@ -645,7 +647,7 @@ void llvm2col::transformPallasAnd(llvm::CallInst &callInstruction, } void llvm2col::transformPallasOr(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { auto *llvmSpecFunc = callInstruction.getCalledFunction(); // Check that the function signature is wellformed @@ -666,7 +668,7 @@ void llvm2col::transformPallasOr(llvm::CallInst &callInstruction, } void llvm2col::transformPallasStar(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { // Check that the function signature is wellformed @@ -689,7 +691,7 @@ void llvm2col::transformPallasStar(llvm::CallInst &callInstruction, } void llvm2col::transformPallasOld(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { auto *llvmSpecFunc = callInstruction.getCalledFunction(); bool isRegularReturn = !llvmSpecFunc->getReturnType()->isVoidTy(); @@ -720,7 +722,7 @@ void llvm2col::transformPallasOld(llvm::CallInst &callInstruction, } void llvm2col::transformPallasBoundVar(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { auto *llvmSpecFunc = callInstruction.getCalledFunction(); bool isRegularReturn = !llvmSpecFunc->getReturnType()->isVoidTy(); @@ -762,7 +764,7 @@ void llvm2col::transformPallasBoundVar(llvm::CallInst &callInstruction, } void llvm2col::transformPallasForall(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { auto *llvmSpecFunc = callInstruction.getCalledFunction(); if (!checkQuantifierSpecFuncWellformed(*llvmSpecFunc, "forall")) { @@ -783,7 +785,7 @@ void llvm2col::transformPallasForall(llvm::CallInst &callInstruction, } void llvm2col::transformPallasSepForall(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { auto *llvmSpecFunc = callInstruction.getCalledFunction(); if (!checkQuantifierSpecFuncWellformed(*llvmSpecFunc, "forall*")) { @@ -805,7 +807,7 @@ void llvm2col::transformPallasSepForall(llvm::CallInst &callInstruction, } void llvm2col::transformPallasExists(llvm::CallInst &callInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { auto *llvmSpecFunc = callInstruction.getCalledFunction(); if (!checkQuantifierSpecFuncWellformed(*llvmSpecFunc, "exists")) { diff --git a/src/llvm/lib/Transform/Instruction/TermOpTransform.cpp b/src/llvm/lib/Transform/Instruction/TermOpTransform.cpp index 4d1420268..7e22571ea 100644 --- a/src/llvm/lib/Transform/Instruction/TermOpTransform.cpp +++ b/src/llvm/lib/Transform/Instruction/TermOpTransform.cpp @@ -3,16 +3,16 @@ #include "Origin/OriginProvider.h" #include "Transform/BlockTransform.h" #include "Transform/Transform.h" +#include "Util/BlockUtils.h" #include "Util/Exceptions.h" #include #include - const std::string SOURCE_LOC = "Transform::Instruction::TermOp"; void llvm2col::transformTermOp(llvm::Instruction &llvmInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { switch (llvm::Instruction::TermOps(llvmInstruction.getOpcode())) { case llvm::Instruction::Ret: @@ -39,9 +39,10 @@ void llvm2col::transformTermOp(llvm::Instruction &llvmInstruction, } void llvm2col::transformRet(llvm::ReturnInst &llvmRetInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { - col::Return *returnStatement = colBlock.add_statements()->mutable_return_(); + col::Return *returnStatement = + colBlock.mutable_terminator()->mutable_return_(); returnStatement->set_allocated_origin( generateSingleStatementOrigin(llvmRetInstruction)); @@ -57,14 +58,11 @@ void llvm2col::transformRet(llvm::ReturnInst &llvmRetInstruction, } void llvm2col::transformConditionalBranch(llvm::BranchInst &llvmBrInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { - col::Branch *colBranch = colBlock.add_statements()->mutable_branch(); + col::Branch *colBranch = colBlock.mutable_terminator()->mutable_branch(); colBranch->set_allocated_origin( generateSingleStatementOrigin(llvmBrInstruction)); - // pre-declare completion because the final branch statement is already - // present - funcCursor.complete(colBlock); /* * I hear you think, why query the 2nd operand? wouldn't that be the false @@ -94,53 +92,17 @@ void llvm2col::transformConditionalBranch(llvm::BranchInst &llvmBrInstruction, *llvmBrInstruction.getCondition(), *colTrueBranch->mutable_v1()); - // Check if the true-branch is empty (i.e. if it jumps directly to a block - // that is also reachable from the false-branch). In that case, we need to - // add an empty block to ensure that assignments of phi-instructions get - // propagated correctly. - bool trueBranchEmpty = - isPotentiallyReachable(llvmFalseBlock, llvmTrueBlock); - if (trueBranchEmpty) { - // Build a new, empty Basic-block as a target for phi-assignments - pallas::LabeledColBlock emptyTrueBlock = - funcCursor.generateIntermediaryLabeledColBlock(llvmBrInstruction); - // Build block that is targeted by the true-branch - pallas::LabeledColBlock originalTrueBlock = - funcCursor.getOrSetLLVMBlock2LabeledColBlockEntry(*llvmTrueBlock); - - // Add the new block to the map of phi-targets - funcCursor.addNewPhiAssignmentTargetBlock( - colBlock, originalTrueBlock.block, emptyTrueBlock.block); - - // Add goto to the empty block - col::Goto *gotoTrueEmpty = colTrueBranch->mutable_v2()->mutable_goto_(); - gotoTrueEmpty->mutable_lbl()->set_id(emptyTrueBlock.bb.label().id()); - gotoTrueEmpty->set_allocated_origin( - generateSingleStatementOrigin(llvmBrInstruction)); - - // Extend the empty bock with a goto to the original target block - col::Goto *gotoTrueOriginal = - emptyTrueBlock.block.add_statements()->mutable_goto_(); - gotoTrueOriginal->mutable_lbl()->set_id( - originalTrueBlock.bb.label().id()); - gotoTrueOriginal->set_allocated_origin( - generateSingleStatementOrigin(llvmBrInstruction)); - // Mark the 'empty' block as completed - funcCursor.complete(emptyTrueBlock.block); - } else { - // get or pre-generate target labeled block - pallas::LabeledColBlock labeledTrueColBlock = - funcCursor.getOrSetLLVMBlock2LabeledColBlockEntry(*llvmTrueBlock); - // goto statement to true block - col::Goto *trueGoto = colTrueBranch->mutable_v2()->mutable_goto_(); - trueGoto->mutable_lbl()->set_id(labeledTrueColBlock.bb.label().id()); - // set origin for goto to true block - trueGoto->set_allocated_origin( - generateSingleStatementOrigin(llvmBrInstruction)); - } + // get or pre-generate target labeled block + col::LlvmBasicBlock &labeledTrueColBlock = + funcCursor.getOrSetLLVMBlock2ColBlockEntry(*llvmTrueBlock); + // goto statement to true block + col::Goto *trueGoto = colTrueBranch->mutable_v2()->mutable_goto_(); + trueGoto->mutable_lbl()->set_id(labeledTrueColBlock.label().id()); + // set origin for goto to true block + trueGoto->set_allocated_origin( + generateSingleStatementOrigin(llvmBrInstruction)); // false branch - // TODO: Implemnt case for empty false-branch (identical to true-branch) col::Tuple2_VctColAstExpr_VctColAstStatement *colFalseBranch = colBranch->add_branches(); // set conditional (which is a true constant as else == else if(true))) @@ -151,55 +113,22 @@ void llvm2col::transformConditionalBranch(llvm::BranchInst &llvmBrInstruction, elseCondition->set_allocated_origin(generateOperandOrigin( llvmBrInstruction, *llvmBrInstruction.getCondition())); - bool falseBranchEmpty = - isPotentiallyReachable(llvmTrueBlock, llvmFalseBlock); - - if (falseBranchEmpty) { - // Build a new, empty Basic-block as a target for phi-assignments - pallas::LabeledColBlock emptyFalseBlock = - funcCursor.generateIntermediaryLabeledColBlock(llvmBrInstruction); - // Build block that is targeted by the false-branch - pallas::LabeledColBlock originalFalseBlock = - funcCursor.getOrSetLLVMBlock2LabeledColBlockEntry(*llvmFalseBlock); - - // Add the new block to the map of phi-targets - funcCursor.addNewPhiAssignmentTargetBlock( - colBlock, originalFalseBlock.block, emptyFalseBlock.block); - - // Add goto to the empty block - col::Goto *gotoFalseEmpty = - colFalseBranch->mutable_v2()->mutable_goto_(); - gotoFalseEmpty->mutable_lbl()->set_id(emptyFalseBlock.bb.label().id()); - gotoFalseEmpty->set_allocated_origin( - generateSingleStatementOrigin(llvmBrInstruction)); - - // Extend the empty bock with a goto to the original target block - col::Goto *gotoFalseOriginal = - emptyFalseBlock.block.add_statements()->mutable_goto_(); - gotoFalseOriginal->mutable_lbl()->set_id( - originalFalseBlock.bb.label().id()); - gotoFalseOriginal->set_allocated_origin( - generateSingleStatementOrigin(llvmBrInstruction)); - // Mark the 'empty' block as completed - funcCursor.complete(emptyFalseBlock.block); - } else { - pallas::LabeledColBlock labeledFalseColBlock = - funcCursor.getOrSetLLVMBlock2LabeledColBlockEntry(*llvmFalseBlock); - // goto statement to false block - col::Goto *falseGoto = colFalseBranch->mutable_v2()->mutable_goto_(); - falseGoto->mutable_lbl()->set_id(labeledFalseColBlock.bb.label().id()); - // set origin for goto to false block - falseGoto->set_allocated_origin( - llvm2col::generateSingleStatementOrigin(llvmBrInstruction)); - } + col::LlvmBasicBlock &labeledFalseColBlock = + funcCursor.getOrSetLLVMBlock2ColBlockEntry(*llvmFalseBlock); + // goto statement to false block + col::Goto *falseGoto = colFalseBranch->mutable_v2()->mutable_goto_(); + falseGoto->mutable_lbl()->set_id(labeledFalseColBlock.label().id()); + // set origin for goto to false block + falseGoto->set_allocated_origin( + llvm2col::generateSingleStatementOrigin(llvmBrInstruction)); - // Transform the blovks of the branches + // Transform the blocks of the branches transformLLVMBlock(*llvmTrueBlock, funcCursor); transformLLVMBlock(*llvmFalseBlock, funcCursor); } void llvm2col::transformUnConditionalBranch( - llvm::BranchInst &llvmBrInstruction, col::Block &colBlock, + llvm::BranchInst &llvmBrInstruction, col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { // get llvm target block auto *llvmTargetBlock = @@ -207,23 +136,21 @@ void llvm2col::transformUnConditionalBranch( // transform llvm targetBlock transformLLVMBlock(*llvmTargetBlock, funcCursor); // get or pre generate target labeled block - pallas::LabeledColBlock labeledColBlock = - funcCursor.getOrSetLLVMBlock2LabeledColBlockEntry(*llvmTargetBlock); + col::LlvmBasicBlock &labeledColBlock = + funcCursor.getOrSetLLVMBlock2ColBlockEntry(*llvmTargetBlock); // create goto to target labeled block - col::Goto *colGoto = colBlock.add_statements()->mutable_goto_(); - colGoto->mutable_lbl()->set_id(labeledColBlock.bb.label().id()); + col::Goto *colGoto = colBlock.mutable_terminator()->mutable_goto_(); + colGoto->mutable_lbl()->set_id(labeledColBlock.label().id()); // set origin of goto statement colGoto->set_allocated_origin( llvm2col::generateSingleStatementOrigin(llvmBrInstruction)); - // pre-declare completion because the final goto is already present - funcCursor.complete(colBlock); } void llvm2col::transformUnreachable( - llvm::UnreachableInst &llvmUnreachableInstruction, col::Block &colBlock, - pallas::FunctionCursor &funcCursor) { + llvm::UnreachableInst &llvmUnreachableInstruction, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { col::LlvmBranchUnreachable *unreachableStatement = - colBlock.add_statements()->mutable_llvm_branch_unreachable(); + colBlock.mutable_terminator()->mutable_llvm_branch_unreachable(); unreachableStatement->set_allocated_origin( generateSingleStatementOrigin(llvmUnreachableInstruction)); unreachableStatement->set_allocated_blame(new col::Blame()); diff --git a/src/llvm/lib/Transform/Instruction/UnaryOpTransform.cpp b/src/llvm/lib/Transform/Instruction/UnaryOpTransform.cpp index a3e25de8a..162b1fab3 100644 --- a/src/llvm/lib/Transform/Instruction/UnaryOpTransform.cpp +++ b/src/llvm/lib/Transform/Instruction/UnaryOpTransform.cpp @@ -3,7 +3,7 @@ const std::string SOURCE_LOC = "Transform::Instruction::UnaryOp"; void llvm2col::transformUnaryOp(llvm::Instruction &llvmInstruction, - col::Block &colBlock, + col::LlvmBasicBlock &colBlock, pallas::FunctionCursor &funcCursor) { // TODO stub reportUnsupportedOperatorError(SOURCE_LOC, llvmInstruction); diff --git a/src/llvm/lib/Transform/LoopContractTransform.cpp b/src/llvm/lib/Transform/LoopContractTransform.cpp index 99b46bc99..2b999760a 100644 --- a/src/llvm/lib/Transform/LoopContractTransform.cpp +++ b/src/llvm/lib/Transform/LoopContractTransform.cpp @@ -172,8 +172,8 @@ bool llvm2col::addInvariantToContract(llvm::MDNode &invMD, llvm::Loop &llvmLoop, llvm2col::generatePallasWrapperCallOrigin(*llvmWFunc, *srcLoc)); local->mutable_ref()->set_id(colVar->id()); } else if (llvm::isa(llvmVal)) { - col::Variable *colVar = &functionCursor.getVariableMapEntry( - *llvmVal, true); + col::Variable *colVar = + &functionCursor.getVariableMapEntry(*llvmVal, true); // Local to var of phi-node auto *local = wrapperCall->add_args()->mutable_local(); local->set_allocated_origin( diff --git a/src/llvm/lib/Util/BlockUtils.cpp b/src/llvm/lib/Util/BlockUtils.cpp new file mode 100644 index 000000000..fb4b92444 --- /dev/null +++ b/src/llvm/lib/Util/BlockUtils.cpp @@ -0,0 +1,9 @@ +#include "Util/BlockUtils.h" + +namespace pallas { + +col::Block &bodyAsBlock(col::LlvmBasicBlock &llvmBB) { + return *llvmBB.mutable_body()->mutable_block(); +} + +} // namespace pallas diff --git a/src/parsers/vct/parsers/parser/ColLLVMParser.scala b/src/parsers/vct/parsers/parser/ColLLVMParser.scala index a2d357149..ddf3479c0 100644 --- a/src/parsers/vct/parsers/parser/ColLLVMParser.scala +++ b/src/parsers/vct/parsers/parser/ColLLVMParser.scala @@ -47,7 +47,7 @@ case class ColLLVMParser( val command = Seq( "opt-17", s"--load-pass-plugin=$pallas", - "--passes=module(pallas-declare-variables,pallas-collect-module-spec),function(pallas-declare-function,pallas-assign-pure,llvm-declare-function-contract,pallas-declare-function-contract,pallas-transform-function-body),module(pallas-print-protobuf)", + "--passes=function(break-crit-edges),module(pallas-declare-variables,pallas-collect-module-spec),function(pallas-declare-function,pallas-assign-pure,llvm-declare-function-contract,pallas-declare-function-contract,pallas-transform-function-body),module(pallas-print-protobuf)", "--disable-output", ) diff --git a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala index 75018b24d..5d2615206 100644 --- a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala @@ -1200,13 +1200,67 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) implicit o: Origin ): Expr[Post] = Result[Post](llvmFunctionMap.ref(ref.decl)) - private def blockToLabel(block: LLVMBasicBlock[Pre]): Statement[Post] = - if (elidedBackEdges.contains(block.label)) { rw.dispatch(block.body) } - else { - Label(rw.labelDecls.dispatch(block.label), rw.dispatch(block.body))( - block.o - ) + def phiTmpVarOrigin() = + Origin(Seq( + PreferredName(Seq("phiTmp")), + LabelContext(s"Generated tmp-var for phi-assignment"), + )) + + def phiTmpVarAssignOrigin() = + Origin(Seq(LabelContext(s"Generated assignment to tmp-var for phi-node"))) + + private def buildPhiAssignments( + basicBlock: LLVMBasicBlock[Pre] + ): Scope[Post] = { + implicit val o: Origin = basicBlock.o + // We split the phi-assignments to ensure that cases where the value + // of a phi-node is used in an assignment to another phi-node get encoded + // correctly. + // I.e. we first generate a block where we assign the values of all + // phi-assignments to temporary variables, and then a block where + // we assign the values of the temporary variables to the actual + // target of the phi-assignment. + var tmpAssignments = Seq[Statement[Post]]() + var phiAssignments = Seq[Statement[Post]]() + var tmpVars = Seq[Variable[Post]]() + basicBlock.phiAssignments.foreach { a => + a match { + case a @ Assign(Local(Ref(targetVar)), expr) => + // Build temporary assignment + val vT = rw.dispatch(getLocalVarType(targetVar)) + val tmpVar = new Variable[Post](vT)(phiTmpVarOrigin()) + tmpVars = tmpVars :+ tmpVar + tmpAssignments = + tmpAssignments :+ Assign( + Local[Post](tmpVar.ref)(phiTmpVarOrigin()), + rw.dispatch(expr), + )(a.blame)(a.o) + // Build assignment of tmp-var to actual var. + phiAssignments = + phiAssignments :+ Assign[Post]( + rw.dispatch(a.target), + Local[Post](tmpVar.ref)(phiTmpVarOrigin()), + )(PanicBlame("Generated assign may not fail"))( + phiTmpVarAssignOrigin() + ) + case _ => throw UnexpectedLLVMNode(a) + } } + val newBlock = Block[Post](tmpAssignments ++ phiAssignments) + Scope[Post](tmpVars, newBlock) + } + + private def blockToLabel(block: LLVMBasicBlock[Pre]): Statement[Post] = { + implicit val o: Origin = block.o + val newBody = Block[Post](Seq( + rw.dispatch(block.body), + buildPhiAssignments(block), + rw.dispatch(block.terminator), + )) + + if (elidedBackEdges.contains(block.label)) { newBody } + else { Label(rw.labelDecls.dispatch(block.label), newBody)(block.o) } + } def rewriteBasicBlock(block: LLVMBasicBlock[Pre]): Statement[Post] = { if (loopBlocks.contains(block)) @@ -1303,26 +1357,22 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) def eliminate(bb: LLVMBasicBlock[Pre]): Block[Post] = { implicit val o: Origin = bb.o - bb.body match { - case block: Block[Pre] => - block.statements.last match { - case goto: Goto[Pre] => - Block[Post]( - block.statements.dropRight(1).map(rw.dispatch) ++ - eliminate(labelDeclMap(goto.lbl.decl)).statements - ) - case _: Return[Pre] => - rw.dispatch(block) match { - case block: Block[Post] => block - case other => throw UnexpectedLLVMNode(other) - } - case branch: Branch[Pre] => - Block[Post]( - block.statements.dropRight(1).map(rw.dispatch) :+ - eliminate(branch) - ) - case other => throw UnexpectedLLVMNode(other) - } + bb.terminator match { + case goto: Goto[Pre] => + Block[Post]( + Seq(rw.dispatch(bb.body), buildPhiAssignments(bb)) ++ + eliminate(labelDeclMap(goto.lbl.decl)).statements + ) + case ret: Return[Pre] => + Block[Post]( + Seq(rw.dispatch(bb.body), buildPhiAssignments(bb), rw.dispatch(ret)) + ) + case branch: Branch[Pre] => + Block[Post](Seq( + rw.dispatch(bb.body), + buildPhiAssignments(bb), + eliminate(branch), + )) case other => throw UnexpectedLLVMNode(other) } } diff --git a/src/rewrite/vct/rewrite/pallas/InlinePallasWrappers.scala b/src/rewrite/vct/rewrite/pallas/InlinePallasWrappers.scala index 20f26be6c..1d9732e81 100644 --- a/src/rewrite/vct/rewrite/pallas/InlinePallasWrappers.scala +++ b/src/rewrite/vct/rewrite/pallas/InlinePallasWrappers.scala @@ -23,12 +23,6 @@ case object InlinePallasWrappers extends RewriterBuilder { LabelContext("Assign of argument during inlining"), )) - private def WrapperInliningOrigin(wrapperDef: Origin, inv: Node[_]): Origin = - Origin( - (LabelContext("inlining of ") +: inv.o.originContents) ++ - (LabelContext("definition") +: wrapperDef.originContents) - ) - case class WrapperInlineFailed(inv: ProcedureInvocation[_], msg: String = "") extends SystemError { override def text: String = { diff --git a/test/main/vct/test/integration/examples/LLVMSpec.scala b/test/main/vct/test/integration/examples/LLVMSpec.scala index 1bff29d0b..2f2503a45 100644 --- a/test/main/vct/test/integration/examples/LLVMSpec.scala +++ b/test/main/vct/test/integration/examples/LLVMSpec.scala @@ -42,4 +42,5 @@ class LLVMSpec extends VercorsSpec { vercors should verify using silicon example "concepts/llvm/pallas/pallas_c_multiply.ll" vercors should verify using silicon example "concepts/llvm/pallas/pallas_c_lower_bound.ll" vercors should fail withCode "notMaintained:false" using silicon example "concepts/llvm/pallas/pallas_c_square_fail.ll" + vercors should verify using silicon example "concepts/llvm/pallas/pallas_c_fibonacci.ll" } diff --git a/test/main/vct/test/integration/helper/ExampleFiles.scala b/test/main/vct/test/integration/helper/ExampleFiles.scala index fd20a1a7e..92ee42385 100644 --- a/test/main/vct/test/integration/helper/ExampleFiles.scala +++ b/test/main/vct/test/integration/helper/ExampleFiles.scala @@ -45,7 +45,8 @@ case object ExampleFiles { "examples/concepts/llvm/pallas/pallas_c_quantifier_fail.c", "examples/concepts/llvm/pallas/pallas_c_multiply.c", "examples/concepts/llvm/pallas/pallas_c_lower_bound.c", - "examples/concepts/llvm/pallas/pallas_c_square_fail.c" + "examples/concepts/llvm/pallas/pallas_c_square_fail.c", + "examples/concepts/llvm/pallas/pallas_c_fibonacci.c" ).map(_.replaceAll("/", File.separator)) val EXCLUSIONS: Seq[Path => Boolean] = Seq(