Add GlobalISel compilation flow to eval scripts.

SSA/Core/Framework/Print.lean

@@ -157,12 +157,13 @@ section ToPrint
 open Std (Format)
 variable {d} [ToPrint d] [DialectSignature d] [Repr d.Op] [Repr d.Ty] [ToString d.Ty] [ToString d.Op]
 
-/-- Format a list of formal arguments as `(%0 : t₀, %1 : t₁, ... %n : tₙ)` -/
+/-- Format a list of formal arguments as `(%0 : t₀, %1 : t₁, ... %n : tₙ)` -/ --here
 partial def formatFormalArgListTuplePrint [ToString d.Ty] (ts : List d.Ty) : String :=
-  let args := (List.range ts.length).zip ts |>.map
+  let args := (List.range ts.length).zip ts.reverse |>.map
     (fun (i, t) => s!"%{i} : {ToPrint.printTy t}")
   "(" ++ String.intercalate ", " args ++ ")"
 
+
 -- Format a sequence of types as `(t₁, ..., tₙ)` using toString instances -/
 private def formatTypeTuplePrint [ToString d.Ty] (xs : List d.Ty) : String :=
   "(" ++ String.intercalate ", " (xs.map ToPrint.printTy) ++ ")"

SSA/Projects/InstCombine/LLVM/EDSL.lean

@@ -40,20 +40,27 @@ In future, this might start throwing errors, if the type is not a bitvec.
 def getVarWidth {Γ : Ctxt (MetaLLVM φ).Ty} : (Σ t, Γ.Var t) → Width φ
   | ⟨.bitvec w, _⟩ => w
 
-def parseOverflowFlags (op : AST.Op φ) : ReaderM φ LLVM.NoWrapFlags :=
-  match op.getAttr? "overflowFlags" with
-  | .none => return {}
-  | .some y => match y with
-    | .opaque_ "llvm.overflow" "nsw" => return ⟨true, false⟩
-    | .opaque_ "llvm.overflow" "nuw" => return ⟨false, true⟩
-    | .opaque_ "llvm.overflow" "none" => return ⟨false, false⟩
-    | .list [.opaque_ "llvm.overflow" "nuw", .opaque_ "llvm.overflow" "nsw"]
-    | .list [.opaque_ "llvm.overflow" "nsw", .opaque_ "llvm.overflow" "nuw"] =>
-        return ⟨true, true⟩
-    | .opaque_ "llvm.overflow" s => throw <| .generic s!"The overflow flag {s} not allowed. \
-        We currently support nsw (no signed wrap) and nuw (no unsigned wrap)"
-    | _ => throw <| .generic s!"Unrecognised overflow flag found: {MLIR.AST.docAttrVal y}. \
-        We currently support nsw (no signed wrap) and nuw (no unsigned wrap)"
+def parseOverflowFlags (op : AST.Op φ) : ReaderM φ LLVM.NoWrapFlags := do
+   match op.getAttr? "overflowFlags" with
+      | .none => return {}
+      | .some y =>
+        match y with
+        | .opaque_ "llvm.overflow" "nsw" => return (⟨true, false⟩)
+        | .opaque_ "llvm.overflow" "nuw" => return (⟨false, true⟩)
+        | .opaque_ "llvm.overflow" "none" => return (⟨false, false⟩)
+        | .list [.opaque_ "llvm.overflow" "nuw", .opaque_ "llvm.overflow" "nsw"]
+        | .list [.opaque_ "llvm.overflow" "nsw", .opaque_ "llvm.overflow" "nuw"] =>
+             return (⟨true, true⟩)
+        | _ =>  /- This case covers generic MLIR syntax for operations with attributes as
+                MLIR encodes them using integer attributes. -/
+              let ⟨n, _ ⟩ ← op.getIntAttr "overflowFlags"
+              match n with
+              | 0 => return (⟨false, false⟩)
+              | 1 => return (⟨true, false⟩)
+              | 2 => return (⟨false, true⟩)
+              | 3 => return (⟨true, true⟩)
+              | s => throw <| .generic s!"The overflow flag with prediacte {s} not allowed. \
+                We currently support nsw (no signed wrap) and nuw (no unsigned wrap)"
 /--
 Maps integer predicate codes (as defined in the MLIR LLVM dialect) to their corresponding
 `LLVM.IntPred` constructors.

SSA/Projects/LLVMRiscV/Evaluation/.gitignore

@@ -0,0 +1,10 @@
+benchmarks/MLIR_single
+benchmarks/MLIR_bb0
+benchmarks/LEANMLIR_ASM
+benchmarks/LLC_ASM
+benchmarks/LLVM
+benchmarks/LLVMIR
+benchmarks/logs
+benchmarks/XDSL_ASM
+benchmarks/XDSL_no_casts
+benchmarks/XDSL_reg_alloc

SSA/Projects/LLVMRiscV/Evaluation/LLVM-tests/add-imm.lean

@@ -31,9 +31,27 @@ def add_positive_low_bound_reject_test: LLVMPeepholeRewriteRefine 32 [Ty.llvm (.
   lhs := add_positive_low_bound_reject_llvm
   rhs := add_positive_low_bound_reject_riscv
 
+<<<<<<< HEAD
+<<<<<<< HEAD
 
 /-- ### add_positive_low_bound_accept -/
 @[simp_denote]
+=======
+=======
+>>>>>>> sarah-eval
+ /-# 2 -/
+/-
+define i32 @add_positive_low_bound_accept(i32 %a) nounwind {
+; RV64I-LABEL: add_positive_low_bound_accept:
+; RV64I:       # %bb.0:
+; RV64I-NEXT:    addi a0, a0, 2047
+; RV64I-NEXT:    addiw a0, a0, 1
+; RV64I-NEXT:    ret
+  %1 = add i32 %a, 2048
+  ret i32 %1
+}
+-/
+>>>>>>> faa6cc524 (first eval run)
 def add_positive_low_bound_accept_llvm := [LV| {
     ^entry (%a: i32):
     %0 = llvm.mlir.constant (2048) : i32
@@ -56,8 +74,26 @@ def add_positive_low_bound_accept_test: LLVMPeepholeRewriteRefine 32 [Ty.llvm (.
   lhs := add_positive_low_bound_accept_llvm
   rhs := add_positive_low_bound_accept_riscv
 
+<<<<<<< HEAD
+<<<<<<< HEAD
 /-- ###  add_positive_high_bound_accept -/
 @[simp_denote]
+=======
+=======
+>>>>>>> sarah-eval
+ /-# 3 -/
+/--
+define i32 @add_positive_high_bound_accept(i32 %a) nounwind {
+; RV64I-LABEL: add_positive_high_bound_accept:
+; RV64I:       # %bb.0:
+; RV64I-NEXT:    addi a0, a0, 2047
+; RV64I-NEXT:    addiw a0, a0, 2047
+; RV64I-NEXT:    ret
+  %1 = add i32 %a, 4094
+  ret i32 %1
+}
+-/
+>>>>>>> faa6cc524 (first eval run)
 def add_positive_high_bound_accept_llvm := [LV| {
     ^entry (%a: i32):
     %0 = llvm.mlir.constant (4094) : i32
@@ -80,9 +116,28 @@ def add_positive_high_bound_accept_test: LLVMPeepholeRewriteRefine 32 [Ty.llvm (
   lhs := add_positive_high_bound_accept_llvm
   rhs := add_positive_high_bound_accept_riscv
 
+<<<<<<< HEAD
+<<<<<<< HEAD
 
 /-- ### add_positive_high_bound_reject -/
 @[simp_denote]
+=======
+=======
+>>>>>>> sarah-eval
+ /-# 4 -/
+/-
+define i32 @add_positive_high_bound_reject(i32 %a) nounwind {
+; RV64I-LABEL: add_positive_high_bound_reject:
+; RV64I:       # %bb.0:
+; RV64I-NEXT:    lui a1, 1
+; RV64I-NEXT:    addi a1, a1, -1
+; RV64I-NEXT:    addw a0, a0, a1
+; RV64I-NEXT:    ret
+  %1 = add i32 %a, 4095
+  ret i32 %1
+}
+-/
+>>>>>>> faa6cc524 (first eval run)
 def add_positive_high_bound_reject_llvm := [LV| {
     ^entry (%a: i32):
     %0 = llvm.mlir.constant (4095) : i32
@@ -107,9 +162,31 @@ def add_positive_high_bound_reject_test: LLVMPeepholeRewriteRefine 32 [Ty.llvm (
   lhs := add_positive_high_bound_reject_llvm
   rhs := add_positive_high_bound_reject_riscv
 
+<<<<<<< HEAD
+<<<<<<< HEAD
 
 /-- ### add_negative_high_bound_reject -/
 @[simp_denote]
+=======
+=======
+>>>>>>> sarah-eval
+ /-# 5 -/
+/-
+define i32 @add_negative_high_bound_reject(i32 %a) nounwind {
+; RV32I-LABEL: add_negative_high_bound_reject:
+; RV32I:       # %bb.0:
+; RV32I-NEXT:    addi a0, a0, -2048
+; RV32I-NEXT:    ret
+;
+; RV64I-LABEL: add_negative_high_bound_reject:
+; RV64I:       # %bb.0:
+; RV64I-NEXT:    addiw a0, a0, -2048
+; RV64I-NEXT:    ret
+  %1 = add i32 %a, -2048
+  ret i32 %1
+}
+-/
+>>>>>>> faa6cc524 (first eval run)
 def add_negative_high_bound_reject_llvm := [LV| {
     ^entry (%a: i32):
     %0 = llvm.mlir.constant (-2048) : i32
@@ -131,9 +208,33 @@ def add_negative_high_bound_reject_test: LLVMPeepholeRewriteRefine 32 [Ty.llvm (
   lhs := add_negative_high_bound_reject_llvm
   rhs := add_negative_high_bound_reject_riscv
 
+<<<<<<< HEAD
+<<<<<<< HEAD
 
 /-- ### add_negative_high_bound_accept -/
 @[simp_denote]
+=======
+=======
+>>>>>>> sarah-eval
+ /-# 6 -/
+/-
+define i32 @add_negative_high_bound_accept(i32 %a) nounwind {
+; RV32I-LABEL: add_negative_high_bound_accept:
+; RV32I:       # %bb.0:
+; RV32I-NEXT:    addi a0, a0, -2048
+; RV32I-NEXT:    addi a0, a0, -1
+; RV32I-NEXT:    ret
+;
+; RV64I-LABEL: add_negative_high_bound_accept:
+; RV64I:       # %bb.0:
+; RV64I-NEXT:    addi a0, a0, -2048
+; RV64I-NEXT:    addiw a0, a0, -1
+; RV64I-NEXT:    ret
+  %1 = add i32 %a, -2049
+  ret i32 %1
+}
+-/
+>>>>>>> faa6cc524 (first eval run)
 def add_negative_high_bound_accept_llvm := [LV| {
   ^entry (%a: i32):
   %0 = llvm.mlir.constant (-2049) : i32
@@ -155,8 +256,26 @@ def add_negative_high_bound_accept_test: LLVMPeepholeRewriteRefine 32 [Ty.llvm (
   lhs := add_negative_high_bound_accept_llvm
   rhs := add_negative_high_bound_accept_riscv
 
+<<<<<<< HEAD
+<<<<<<< HEAD
 /-- ### add_negative_low_bound_accept -/
 @[simp_denote]
+=======
+=======
+>>>>>>> sarah-eval
+ /-# 7 -/
+/-
+define i32 @add_negative_low_bound_accept(i32 %a) nounwind {
+; RV64I-LABEL: add_negative_low_bound_accept:
+; RV64I:       # %bb.0:
+; RV64I-NEXT:    addi a0, a0, -2048
+; RV64I-NEXT:    addiw a0, a0, -2048
+; RV64I-NEXT:    ret
+  %1 = add i32 %a, -4096
+  ret i32 %1
+}
+-/
+>>>>>>> faa6cc524 (first eval run)
 def add_negative_low_bound_accept_llvm := [LV| {
   ^entry (%a: i32):
   %0 = llvm.mlir.constant (-4096) : i32
@@ -178,8 +297,27 @@ def add_negative_low_bound_accept_test : LLVMPeepholeRewriteRefine 32 [Ty.llvm (
   lhs := add_negative_low_bound_accept_llvm
   rhs := add_negative_low_bound_accept_riscv
 
+<<<<<<< HEAD
+<<<<<<< HEAD
 /-- ###  add_negative_low_bound_reject -/
 @[simp_denote]
+=======
+=======
+>>>>>>> sarah-eval
+ /-# 8 -/
+/-
+define i32 @add_negative_low_bound_reject(i32 %a) nounwind {
+; RV64I-LABEL: add_negative_low_bound_reject:
+; RV64I:       # %bb.0:
+; RV64I-NEXT:    lui a1, 1048575
+; RV64I-NEXT:    addi a1, a1, -1
+; RV64I-NEXT:    addw a0, a0, a1
+; RV64I-NEXT:    ret
+  %1 = add i32 %a, -4097
+  ret i32 %1
+}
+-/
+>>>>>>> faa6cc524 (first eval run)
 def add_negative_low_bound_reject_llvm := [LV| {
   ^entry (%a: i32):
   %0 = llvm.mlir.constant (-4097) : i32
@@ -203,8 +341,26 @@ def add_negative_low_bound_reject_test : LLVMPeepholeRewriteRefine 32 [Ty.llvm (
   lhs := add_negative_low_bound_reject_llvm
   rhs := add_negative_low_bound_reject_riscv
 
+<<<<<<< HEAD
+<<<<<<< HEAD
 /-- ###  add32_accept -/
 @[simp_denote]
+=======
+=======
+>>>>>>> sarah-eval
+ /-# 9 -/
+/-
+define i32 @add32_accept(i32 %a) nounwind {
+; RV64I-LABEL: add32_accept:
+; RV64I:       # %bb.0:
+; RV64I-NEXT:    addi a0, a0, 2047
+; RV64I-NEXT:    addiw a0, a0, 952
+; RV64I-NEXT:    ret
+  %1 = add i32 %a, 2999
+  ret i32 %1
+}
+-/
+>>>>>>> faa6cc524 (first eval run)
 def add32_accept_llvm := [LV| {
   ^entry (%a: i32):
   %0 = llvm.mlir.constant (2999) : i32
@@ -226,8 +382,26 @@ def add32_accept_test : LLVMPeepholeRewriteRefine 32 [Ty.llvm (.bitvec 32)] wher
   lhs := add32_accept_llvm
   rhs := add32_accept_riscv
 
+<<<<<<< HEAD
+<<<<<<< HEAD
 /-- ###  add32_sext_accept -/
 @[simp_denote]
+=======
+=======
+>>>>>>> sarah-eval
+ /-# 10 -/
+/-
+define signext i32 @add32_sext_accept(i32 signext %a) nounwind {
+; RV64I-LABEL: add32_sext_accept:
+; RV64I:       # %bb.0:
+; RV64I-NEXT:    addi a0, a0, 2047
+; RV64I-NEXT:    addiw a0, a0, 952
+; RV64I-NEXT:    ret
+  %1 = add i32 %a, 2999
+  ret i32 %1
+}
+-/
+>>>>>>> faa6cc524 (first eval run)
 def add32_sext_accept_llvm := [LV| {
   ^entry (%a: i32):
   %0 = llvm.mlir.constant (2999) : i32
@@ -249,9 +423,26 @@ def add32_sext_accept_test : LLVMPeepholeRewriteRefine 32 [Ty.llvm (.bitvec 32)]
   lhs := add32_sext_accept_llvm
   rhs :=  add32_sext_accept_riscv
 
+<<<<<<< HEAD
+<<<<<<< HEAD
 
 /-- ### add64_accept -/
 @[simp_denote]
+=======
+=======
+>>>>>>> sarah-eval
+ /-# 11 -/
+/-define i64 @add64_accept(i64 %a) nounwind {
+; RV64I-LABEL: add64_accept:
+; RV64I:       # %bb.0:
+; RV64I-NEXT:    addi a0, a0, 2047
+; RV64I-NEXT:    addi a0, a0, 952
+; RV64I-NEXT:    ret
+  %1 = add i64 %a, 2999
+  ret i64 %1
+}
+-/
+>>>>>>> faa6cc524 (first eval run)
 def add64_accept_llvm := [LV| {
   ^entry (%a: i64):
   %0 = llvm.mlir.constant (2999) : i64