feat(io): CTree Interpreter for I/O

.github/dependabot.yml

@@ -0,0 +1,10 @@
+version: 2
+updates:
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    schedule:
+      interval: "monthly"
+    groups:
+      github-actions:
+        patterns:
+          - "*"

.github/workflows/ci.yml

@@ -14,19 +14,19 @@ jobs:
   build-docs:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
 
       - name: Build docs
         continue-on-error: true
-        uses: leanprover/lean-action@v1
+        uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1.6.0
         with:
           lake-package-directory: "docbuild"
           build-args: "Veir:docs"
 
       - name: Upload docs artifact
         if: github.ref == 'refs/heads/main'
         continue-on-error: true
-        uses: actions/upload-artifact@v4
+        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
         with:
           name: docs
           path: docbuild/.lake/build/doc/
@@ -37,12 +37,12 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout gh-pages branch
-        uses: actions/checkout@v4
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
         with:
           ref: gh-pages
 
       - name: Download docs artifact
-        uses: actions/download-artifact@v4
+        uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
         continue-on-error: true
         with:
           name: docs

.github/workflows/lean_action_ci.yml

@@ -13,10 +13,10 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
 
       - name: Set up Python 3.13
-        uses: actions/setup-python@v6
+        uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7.0.0
         with:
           python-version: 3.13
 
@@ -33,7 +33,7 @@ jobs:
         buildType: [release, debug]
 
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
 
       # `buildType` is a lakefile field with no command-line override, so the
       # debug run edits it in place. The `grep` is not redundant: if the field
@@ -49,15 +49,15 @@ jobs:
         run: source .envrc
 
       - name: Add LLVM apt repository
-        uses: gerlero/add-apt-repository@v1
+        uses: gerlero/add-apt-repository@397d907a67c29d276af289f5e9574375b8fc7481 # v1.1.0
         with:
           uri: http://apt.llvm.org/noble/ 
           key: https://apt.llvm.org/llvm-snapshot.gpg.key
           component: main
           suite: llvm-toolchain-noble-22
 
       - name: Install mlir-opt
-        uses: gerlero/apt-install@v1
+        uses: gerlero/apt-install@c0fa73fe5c4a22deecf6d629565be92a15dd2026 # v1.3.12
         with:
           packages: mlir-22-tools
 
@@ -66,25 +66,25 @@ jobs:
           sudo ln -s /usr/bin/mlir-opt-22 /usr/bin/mlir-opt
 
       - name: Build the project
-        uses: leanprover/lean-action@v1
+        uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1.6.0
         with:
           build-args: "--iofail"
           test: false
 
       - name: Run unit tests
-        uses: leanprover/lean-action@v1
+        uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1.6.0
         with:
           test-args: "--iofail"
           test: true
 
       - name: Install uv
-        uses: astral-sh/setup-uv@v7
+        uses: astral-sh/setup-uv@20cfd1bf945f4377ade1205e4dbc17946fc9a30d # v10.0.1
         with:
           enable-cache: true
           cache-dependency-glob: "uv.lock"
 
       - name: Set up Python 3.13
-        uses: actions/setup-python@v6
+        uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7.0.0
         with:
           python-version: 3.13
 
@@ -95,7 +95,7 @@ jobs:
         run: uv run lit Test/ -v
 
       - name: Build the ExArray package
-        uses: leanprover/lean-action@v1
+        uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1.6.0
         with:
           lake-package-directory: "ExArray"
 

.github/workflows/lean_action_ci_namespace.yml

@@ -18,7 +18,7 @@ jobs:
     runs-on: namespace-profile-veir
 
     steps:
-      - uses: namespacelabs/nscloud-checkout-action@v9
+      - uses: namespacelabs/nscloud-checkout-action@66f2dc6f6c42a8ac6c4e53473c4840006822831e # v9.0.1
 
       # The checkout wipes the workspace, so `.lake` does not exist when the
       # cache action runs and it has nothing to bind the volume onto. It skips
@@ -30,7 +30,7 @@ jobs:
       # `~/.elan` holds the Lean toolchain and `.lake` the build tree; together
       # they dominate the run.
       - name: Set up caches
-        uses: namespacelabs/nscloud-cache-action@v1
+        uses: namespacelabs/nscloud-cache-action@c5f8dab7560444c4bf8dbc64f1b203431873c547 # v1.6.1
         with:
           path: |
             ~/.elan
@@ -39,7 +39,7 @@ jobs:
       # One invocation: `lean-action` runs `lake build` and then `lake test`,
       # so a second one only repeated the build as a no-op.
       - name: Build and test the project
-        uses: leanprover/lean-action@v1
+        uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1.6.0
         with:
           build-args: "--iofail"
           test-args: "--iofail"

.github/workflows/nightly-veir-tests.yml

@@ -11,10 +11,10 @@ jobs:
 
 
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
 
       - name: Build veir
-        uses: leanprover/lean-action@v1
+        uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1.6.0
         with:
           build-args: "--iofail"
 
@@ -25,13 +25,13 @@ jobs:
           echo "/usr/lib/llvm-20/bin" >> $GITHUB_PATH
 
       - name: Clone veir-tests
-        uses: actions/checkout@v4
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
         with:
           repository: opencompl/veir-tests
           path: veir-tests
 
       - name: Set up Python
-        uses: actions/setup-python@v6
+        uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7.0.0
         with:
           python-version: '3.13'
 

Test/Cir/invalid_const_other_type.mlir

@@ -0,0 +1,7 @@
+// RUN: not veir-opt --allow-unregistered-dialect %s 2>&1 | filecheck %s
+
+// An unmodelled constant value still has to agree with the result type when it carries one.
+// CHECK: cir.const: Expected result type to match the constant's type
+"builtin.module"() ({
+  %0 = "cir.const"() <{value = #cir.ptr<null> : !cir.ptr<!cir.int<s, 32>>}> : () -> !cir.int<s, 32>
+}) : () -> ()

Test/Cir/unmodelled.mlir

@@ -0,0 +1,25 @@
+// RUN: VEIR_UNREGISTERED_ROUNDTRIP
+
+// ClangIR pieces VeIR does not model. A registered `cir` operation in an unmodelled
+// variant (a pointer or float constant, a pointer comparison, a float select) is accepted
+// and printed back verbatim; an unknown operation falls back to `builtin.unregistered`.
+"builtin.module"() ({
+  "cir.func"() <{function_type = !cir.func<(!cir.ptr<!cir.int<s, 32>>) -> !cir.bool>, sym_name = "unmodelled"}> ({
+  ^bb0(%p : !cir.ptr<!cir.int<s, 32>>):
+    %null = "cir.const"() <{value = #cir.ptr<null> : !cir.ptr<!cir.int<s, 32>>}> : () -> !cir.ptr<!cir.int<s, 32>>
+    %f = "cir.const"() <{value = #cir.fp<1.500000e+00> : !cir.double}> : () -> !cir.double
+    %eq = "cir.cmp"(%p, %null) <{kind = 4 : i32}> : (!cir.ptr<!cir.int<s, 32>>, !cir.ptr<!cir.int<s, 32>>) -> !cir.bool
+    %sel = "cir.select"(%eq, %f, %f) : (!cir.bool, !cir.double, !cir.double) -> !cir.double
+    %g = "cir.get_global"() <{name = @counter}> : () -> !cir.ptr<!cir.int<s, 32>>
+    "cir.return"(%eq) : (!cir.bool) -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK:      "cir.func"() <{"function_type" = !cir.func<(!cir.ptr<!cir.int<s, 32>>) -> !cir.bool>, "sym_name" = "unmodelled"}> ({
+// CHECK-NEXT: ^{{.*}}(%{{.*}} : !cir.ptr<!cir.int<s, 32>>):
+// CHECK-NEXT: %{{.*}} = "cir.const"() <{"value" = #cir.ptr<null> : !cir.ptr<!cir.int<s, 32>>}> : () -> !cir.ptr<!cir.int<s, 32>>
+// CHECK-NEXT: %{{.*}} = "cir.const"() <{"value" = #cir.fp<1.500000e+00> : !cir.double}> : () -> !cir.double
+// CHECK-NEXT: %{{.*}} = "cir.cmp"(%{{.*}}, %{{.*}}) <{"kind" = 4 : i32}> : (!cir.ptr<!cir.int<s, 32>>, !cir.ptr<!cir.int<s, 32>>) -> !cir.bool
+// CHECK-NEXT: %{{.*}} = "cir.select"(%{{.*}}, %{{.*}}, %{{.*}}) : (!cir.bool, !cir.double, !cir.double) -> !cir.double
+// CHECK-NEXT: %{{.*}} = "cir.get_global"() <{"name" = @counter}> : () -> !cir.ptr<!cir.int<s, 32>>
+// CHECK-NEXT: "cir.return"(%{{.*}}) : (!cir.bool) -> ()

Test/HW/instance.mlir

@@ -0,0 +1,30 @@
+// RUN: VEIR_ROUNDTRIP
+
+"builtin.module"() ({
+  "hw.module"() <{comment = "", module_type = !hw.modty<input a : i8, input b : i8, output out : i8>, parameters = [], per_port_attrs = [], result_locs = [loc(unknown)], sym_name = "add2"}> ({
+  ^bb0(%arg3: i8, %arg4: i8):
+    %2 = "comb.add"(%arg3, %arg4) : (i8, i8) -> i8
+    "hw.output"(%2) : (i8) -> ()
+  }) {sym_visibility = "private"} : () -> ()
+  "hw.module"() <{comment = "", module_type = !hw.modty<input a : i8, input b : i8, input c : i8, output out : i8>, parameters = [], per_port_attrs = [], result_locs = [loc(unknown)], sym_name = "add3"}> ({
+  ^bb0(%arg0: i8, %arg1: i8, %arg2: i8):
+    %0 = "hw.instance"(%arg0, %arg1) <{argNames = ["a", "b"], instanceName = "a0", moduleName = @add2, parameters = [], resultNames = ["out"]}> {sv.namehint = "s"} : (i8, i8) -> i8
+    %1 = "hw.instance"(%arg2, %0) <{argNames = ["a", "b"], instanceName = "a1", moduleName = @add2, parameters = [], resultNames = ["out"]}> : (i8, i8) -> i8
+    "hw.output"(%1) : (i8) -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK:      "builtin.module"() ({
+// CHECK-NEXT:   ^{{.*}}():
+// CHECK-NEXT:     "hw.module"() <{"module_type" = !hw.modty<input a : i8, input b : i8, output out : i8>, "parameters" = [], "per_port_attrs" = [], "sym_name" = "add2"}> ({
+// CHECK-NEXT:       ^{{.*}}(%{{.*}} : i8, %{{.*}} : i8):
+// CHECK-NEXT:         %{{.*}} = "comb.add"(%{{.*}}, %{{.*}}) : (i8, i8) -> i8
+// CHECK-NEXT:         "hw.output"(%{{.*}}) : (i8) -> ()
+// CHECK-NEXT:     }) {"sym_visibility" = "private"} : () -> ()
+// CHECK-NEXT:     "hw.module"() <{"module_type" = !hw.modty<input a : i8, input b : i8, input c : i8, output out : i8>, "parameters" = [], "per_port_attrs" = [], "sym_name" = "add3"}> ({
+// CHECK-NEXT:       ^{{.*}}(%{{.*}} : i8, %{{.*}} : i8, %{{.*}} : i8):
+// CHECK-NEXT:         %{{.*}} = "hw.instance"(%{{.*}}, %{{.*}}) <{"argNames" = ["a", "b"], "instanceName" = "a0", "moduleName" = @add2, "parameters" = [], "resultNames" = ["out"]}> {"sv.namehint" = "s"} : (i8, i8) -> i8
+// CHECK-NEXT:         %{{.*}} = "hw.instance"(%{{.*}}, %{{.*}}) <{"argNames" = ["a", "b"], "instanceName" = "a1", "moduleName" = @add2, "parameters" = [], "resultNames" = ["out"]}> : (i8, i8) -> i8
+// CHECK-NEXT:         "hw.output"(%{{.*}}) : (i8) -> ()
+// CHECK-NEXT:     }) : () -> ()
+// CHECK-NEXT: }) : () -> ()

Test/IO/rand_non_integer_length.mlir

@@ -0,0 +1,11 @@
+// RUN: not veir-opt %s 2>&1 | filecheck %s
+
+"builtin.module"() ({
+  "func.func"() <{sym_name = "main", function_type = () -> ()}> ({
+    %len = "llvm.mlir.constant"() <{value = 4 : i64}> : () -> i64
+    %buf = "llvm.alloca"(%len) <{elem_type = i8}> : (i64) -> !llvm.ptr
+    %n = "io.rand"(%buf, %buf) : (!llvm.ptr, !llvm.ptr) -> i64
+    // CHECK: io.rand: Expected operand 1 to have integer type
+    "func.return"() : () -> ()
+  }) : () -> ()
+}) : () -> ()

Test/IO/rand_with_address.mlir

@@ -0,0 +1,12 @@
+// RUN: not veir-opt %s 2>&1 | filecheck %s
+
+"builtin.module"() ({
+  "func.func"() <{sym_name = "main", function_type = () -> ()}> ({
+    %peer = "test.test"() : () -> !io.address
+    %len = "llvm.mlir.constant"() <{value = 4 : i64}> : () -> i64
+    %buf = "llvm.alloca"(%len) <{elem_type = i8}> : (i64) -> !llvm.ptr
+    %n = "io.rand"(%peer, %buf, %len) : (!io.address, !llvm.ptr, i64) -> i64
+    // CHECK: io.rand: Expected 2 operand(s)
+    "func.return"() : () -> ()
+  }) : () -> ()
+}) : () -> ()

Test/IO/recv_non_address_result.mlir

@@ -0,0 +1,11 @@
+// RUN: not veir-opt %s 2>&1 | filecheck %s
+
+"builtin.module"() ({
+  "func.func"() <{sym_name = "main", function_type = () -> ()}> ({
+    %len = "llvm.mlir.constant"() <{value = 4 : i64}> : () -> i64
+    %buf = "llvm.alloca"(%len) <{elem_type = i8}> : (i64) -> !llvm.ptr
+    %n, %from = "io.recv"(%buf, %len) : (!llvm.ptr, i64) -> (i64, i32)
+    // CHECK: io.recv: Expected result 1 to have !io.address type
+    "func.return"() : () -> ()
+  }) : () -> ()
+}) : () -> ()

Test/IO/recv_non_i64_result.mlir

@@ -0,0 +1,11 @@
+// RUN: not veir-opt %s 2>&1 | filecheck %s
+
+"builtin.module"() ({
+  "func.func"() <{sym_name = "main", function_type = () -> ()}> ({
+    %len = "llvm.mlir.constant"() <{value = 4 : i64}> : () -> i64
+    %buf = "llvm.alloca"(%len) <{elem_type = i8}> : (i64) -> !llvm.ptr
+    %n, %from = "io.recv"(%buf, %len) : (!llvm.ptr, i64) -> (i32, !io.address)
+    // CHECK: io.recv: Expected result 0 to have i64 type
+    "func.return"() : () -> ()
+  }) : () -> ()
+}) : () -> ()

Test/IO/recv_non_pointer_buffer.mlir

@@ -0,0 +1,10 @@
+// RUN: not veir-opt %s 2>&1 | filecheck %s
+
+"builtin.module"() ({
+  "func.func"() <{sym_name = "main", function_type = () -> ()}> ({
+    %len = "llvm.mlir.constant"() <{value = 4 : i64}> : () -> i64
+    %n, %from = "io.recv"(%len, %len) : (i64, i64) -> (i64, !io.address)
+    // CHECK: io.recv: Expected operand 0 to have !llvm.ptr type
+    "func.return"() : () -> ()
+  }) : () -> ()
+}) : () -> ()

Test/IO/roundtrip.mlir

@@ -0,0 +1,24 @@
+// RUN: VEIR_ROUNDTRIP
+
+"builtin.module"() ({
+  // CHECK:      "builtin.module"() ({
+  // CHECK-NEXT:   ^{{.*}}():
+  "func.func"() <{sym_name = "main", function_type = () -> ()}> ({
+    // CHECK-NEXT:     "func.func"() <{"function_type" = () -> (), "sym_name" = "main"}> ({
+    // CHECK-NEXT:       ^{{.*}}():
+    %peer = "io.self"() : () -> !io.address
+    // CHECK-NEXT:         %[[peer:.*]] = "io.self"() : () -> !io.address
+    %len = "llvm.mlir.constant"() <{value = 32 : i64}> : () -> i64
+    // CHECK-NEXT:         %[[len:.*]] = "llvm.mlir.constant"() <{"value" = 32 : i64}> : () -> i64
+    %buf = "llvm.alloca"(%len) <{elem_type = i8}> : (i64) -> !llvm.ptr
+    // CHECK-NEXT:         %[[buf:.*]] = "llvm.alloca"(%[[len]]) <{"alignment" = 0 : i64, "elem_type" = i8}> : (i64) -> !llvm.ptr
+    %n0 = "io.rand"(%buf, %len) : (!llvm.ptr, i64) -> i64
+    // CHECK-NEXT:         %{{.*}} = "io.rand"(%[[buf]], %[[len]]) : (!llvm.ptr, i64) -> i64
+    %n1 = "io.send"(%peer, %buf, %len) : (!io.address, !llvm.ptr, i64) -> i64
+    // CHECK-NEXT:         %{{.*}} = "io.send"(%[[peer]], %[[buf]], %[[len]]) : (!io.address, !llvm.ptr, i64) -> i64
+    %n2, %from = "io.recv"(%buf, %len) : (!llvm.ptr, i64) -> (i64, !io.address)
+    // CHECK-NEXT:         %{{.*}}:2 = "io.recv"(%[[buf]], %[[len]]) : (!llvm.ptr, i64) -> (i64, !io.address)
+    "func.return"() : () -> ()
+    // CHECK-NEXT:         "func.return"() : () -> ()
+  }) : () -> ()
+}) : () -> ()

Test/IO/self_non_address_result.mlir

@@ -0,0 +1,9 @@
+// RUN: not veir-opt %s 2>&1 | filecheck %s
+
+"builtin.module"() ({
+  "func.func"() <{sym_name = "main", function_type = () -> ()}> ({
+    %a = "io.self"() : () -> i32
+    // CHECK: io.self: Expected result 0 to have !io.address type
+    "func.return"() : () -> ()
+  }) : () -> ()
+}) : () -> ()

Test/IO/send_int_destination.mlir

@@ -0,0 +1,12 @@
+// RUN: not veir-opt %s 2>&1 | filecheck %s
+
+"builtin.module"() ({
+  "func.func"() <{sym_name = "main", function_type = () -> ()}> ({
+    %len = "llvm.mlir.constant"() <{value = 4 : i64}> : () -> i64
+    %buf = "llvm.alloca"(%len) <{elem_type = i8}> : (i64) -> !llvm.ptr
+    %dest = "arith.constant"() <{value = 7 : i32}> : () -> i32
+    %n = "io.send"(%dest, %buf, %len) : (i32, !llvm.ptr, i64) -> i64
+    // CHECK: io.send: Expected operand 0 to have !io.address type
+    "func.return"() : () -> ()
+  }) : () -> ()
+}) : () -> ()

Test/IO/send_non_i64_result.mlir

@@ -0,0 +1,12 @@
+// RUN: not veir-opt %s 2>&1 | filecheck %s
+
+"builtin.module"() ({
+  "func.func"() <{sym_name = "main", function_type = () -> ()}> ({
+    %peer = "test.test"() : () -> !io.address
+    %len = "llvm.mlir.constant"() <{value = 4 : i64}> : () -> i64
+    %buf = "llvm.alloca"(%len) <{elem_type = i8}> : (i64) -> !llvm.ptr
+    %n = "io.send"(%peer, %buf, %len) : (!io.address, !llvm.ptr, i64) -> i32
+    // CHECK: io.send: Expected result 0 to have i64 type
+    "func.return"() : () -> ()
+  }) : () -> ()
+}) : () -> ()

Test/IO/send_non_integer_length.mlir

@@ -0,0 +1,12 @@
+// RUN: not veir-opt %s 2>&1 | filecheck %s
+
+"builtin.module"() ({
+  "func.func"() <{sym_name = "main", function_type = () -> ()}> ({
+    %peer = "test.test"() : () -> !io.address
+    %len = "llvm.mlir.constant"() <{value = 4 : i64}> : () -> i64
+    %buf = "llvm.alloca"(%len) <{elem_type = i8}> : (i64) -> !llvm.ptr
+    %n = "io.send"(%peer, %buf, %buf) : (!io.address, !llvm.ptr, !llvm.ptr) -> i64
+    // CHECK: io.send: Expected operand 2 to have integer type
+    "func.return"() : () -> ()
+  }) : () -> ()
+}) : () -> ()