Added unclonable record and anvil.{hls, test} annotation support.

sireum · Mar 9, 2025 · 71ccb1d · 71ccb1d
1 parent ad6c985
commit 71ccb1d
Show file tree

Hide file tree

Showing 4 changed files with 14 additions and 75 deletions.
diff --git a/jvm/src/test/scala/org/sireum/anvil/IRSimulatorTest.scala b/jvm/src/test/scala/org/sireum/anvil/IRSimulatorTest.scala
@@ -74,7 +74,7 @@ class IRSimulatorTest extends SireumRcSpec {
           override def string: String = "AnvilTest.Output"
         }, reporter) match {
           case Some(ir) =>
-            val state = IRSimulator.State.Ext.create(ir.anvil.config.memory, ir.maxRegisters)
+            val state = IRSimulator.State.create(ir.anvil.config.memory, ir.maxRegisters)
             IRSimulator(ir.anvil).evalProcedure(state, ir.procedure)
             val displaySize = ir.anvil.config.printSize
             val offset = ir.globalInfoMap.get(Anvil.displayName).get.offset + ir.anvil.spTypeByteSize +

diff --git a/jvm/src/test/scala/org/sireum/anvil/example/add-test.sc b/jvm/src/test/scala/org/sireum/anvil/example/add-test.sc
@@ -2,10 +2,10 @@
 import org.sireum._
 import org.sireum.U16._
 
-def add(x: U16, y: U16): U16 = {
+@anvil.hls def add(x: U16, y: U16): U16 = {
   return x + y
 }
 
-def testAdd(): Unit = {
+@anvil.test def testAdd(): Unit = {
   println(add(u16"3", u16"5"))
 }
diff --git a/shared/src/main/scala/org/sireum/anvil/IRSimulator.scala b/shared/src/main/scala/org/sireum/anvil/IRSimulator.scala
@@ -28,14 +28,11 @@ package org.sireum.anvil
 
 import org.sireum._
 import org.sireum.lang.{ast => AST}
+import org.sireum.U8._
 import org.sireum.U64._
 
 object IRSimulator {
-  @msig trait State {
-    def memory: MSZ[U8]
-
-    def temps: MSZ[U64]
-
+  @record @unclonable class State(val memory: MSZ[U8], val temps: MSZ[U64]) {
     def cpIndex: Z = {
       return temps.size - 3
     }
@@ -134,9 +131,7 @@ object IRSimulator {
       }
     }
 
-    @ext("State_Ext") object Ext {
-      @pure def create(memory: Z, temps: Z): State = $
-    }
+    @strictpure def create(memory: Z, temps: Z): State = State(MSZ.create(memory, u8"0"), MSZ.create(temps + 3, u64"0"))
 
   }
 
@@ -815,14 +810,9 @@ import IRSimulator._
     }
   }
 
-  @pure def evalBlock(state: State, b: AST.IR.BasicBlock): Unit = {
-    val edits = ops.ISZOps((for (g <- b.grounds) yield evalGroundOrJump(Either.Left(g))) :+
+  @pure def evalBlock(state: State, b: AST.IR.BasicBlock): ISZ[State.Edit] = {
+    return ops.ISZOps((for (g <- b.grounds) yield evalGroundOrJump(Either.Left(g))) :+
       evalGroundOrJump(Either.Right(b.jump))).parMapUnordered((f: State => State.Edit) => f(state))
-    var i = 0
-    while (i < edits.size) {
-      edits(i).update(state)
-      i = i + 1
-    }
   }
 
   def evalProcedure(state: State, p: AST.IR.Procedure): Unit = {
@@ -845,7 +835,12 @@ import IRSimulator._
     while (state.CP != u64"0" && state.CP != u64"1") {
       val b = blockMap.get(state.CP).get
       //log("Evaluating", b)
-      evalBlock(state, b)
+      val edits = evalBlock(state, b)
+      var i = 0
+      while (i < edits.size) {
+        edits(i).update(state)
+        i = i + 1
+      }
     }
 
     //println(s"End state: $state")

diff --git a/shared/src/main/scala/org/sireum/anvil/State_Ext.scala b/shared/src/main/scala/org/sireum/anvil/State_Ext.scala